5ed857b · Idris-dev · git.iko.soy

CHANGELOG+2

@@ -40,6 +40,8 @@ New in 0.9.17:

4040* Classes can now be annotated with 'determining parameters' to say which

4141 must be available before resolving instances. Only determining parameters

4242 are checked when checking for overlapping instances.

43+* Arguments to class instances are now checked for injectivity.

44+ Unification assumes this, so we need to check when instances are defined.

4345

4446New in 0.9.16:

4547--------------

idris.cabal+3

@@ -289,6 +289,9 @@ Extra-source-files:

289289 test/reg058/run

290290 test/reg058/*.idr

291291 test/reg058/expected

292+ test/reg059/run

293+ test/reg059/*.idr

294+ test/reg059/expected

292295

293296 test/basic001/run

294297 test/basic001/*.idr

libs/base/Language/Reflection/Utils.idr+1

@@ -270,6 +270,7 @@ instance Show Err where

270270 show (NoTypeDecl n) = "NoTypeDecl " ++ show n

271271 show (NotInjective tm tm' x) = "NotInjective " ++ show tm ++ " " ++ show tm'

272272 show (CantResolve tm) = "CantResolve " ++ show tm

273+ show (InvalidTCArg n tm) = "InvalidTCName " ++ show n ++ " (" ++ show tm ++ ")"

273274 show (CantResolveAlts xs) = "CantResolveAlts " ++ show xs

274275 show (IncompleteTerm tm) = "IncompleteTerm " ++ show tm

275276 show (NoEliminator s tm) = "NoEliminator " ++ show s ++ " " ++ show tm

libs/prelude/Language/Reflection/Errors.idr+1

@@ -29,6 +29,7 @@ data Err = Msg String

2929 | NoTypeDecl TTName

3030 | NotInjective TT TT TT

3131 | CantResolve TT

32+ | InvalidTCArg TTName TT

3233 | CantResolveAlts (List TTName)

3334 | IncompleteTerm TT

3435 | NoEliminator String TT

libs/prelude/Prelude/Applicative.idr−4

@@ -15,10 +15,6 @@ class Functor f => Applicative (f : Type -> Type) where

1515 pure : a -> f a

1616 (<*>) : f (a -> b) -> f a -> f b

1717

18−instance Applicative id where

19− pure a = a

20− f <*> a = f a

21−

2218class (Applicative f, VerifiedFunctor f) => VerifiedApplicative (f : Type -> Type) where

2319 applicativeMap : (x : f a) -> (g : a -> b) ->

2420 map g x = pure g <*> x

libs/prelude/Prelude/Functor.idr−2

@@ -24,5 +24,3 @@ class Functor f => VerifiedFunctor (f : Type -> Type) where

2424 (g1 : a -> b) -> (g2 : b -> c) ->

2525 map (g2 . g1) x = (map g2 . map g1) x

2626

27−instance Functor id where

28− map f a = f a

libs/prelude/Prelude/Monad.idr−3

@@ -24,9 +24,6 @@ class (Monad m, VerifiedApplicative m) => VerifiedMonad (m : Type -> Type) where

2424 monadAssociativity : (mx : m a) -> (f : a -> m b) -> (g : b -> m c) ->

2525 (mx >>= f) >>= g = mx >>= (\x => f x >>= g)

2626

27−instance Monad id where

28− a >>= f = f a

29−

3027||| Also called `join` or mu

3128flatten : Monad m => m (m a) -> m a

3229flatten a = a >>= id

rts/idris_gc.c+3−14

@@ -112,19 +112,8 @@ void idris_gc(VM* vm) {

112112 if (vm->heap.old != NULL)

113113 free(vm->heap.old);

114114

115− char* newheap = malloc(vm->heap.size);

116− char* oldheap = vm->heap.heap;

117−

118− vm->heap.heap = newheap;

119−#ifdef FORCE_ALIGNMENT

120− if (((i_int)(vm->heap.heap)&1) == 1) {

121− vm->heap.next = newheap + 1;

122− } else

123−#endif

124− {

125− vm->heap.next = newheap;

126− }

127− vm->heap.end = newheap + vm->heap.size;

115+ /* Allocate swap heap. */

116+ alloc_heap(&vm->heap, vm->heap.size, vm->heap.growth, vm->heap.heap);

128117

129118 VAL* root;

130119

@@ -139,6 +128,7 @@ void idris_gc(VM* vm) {

139128 msg->msg = copy(vm, msg->msg);

140129 }

141130#endif

131+

142132 vm->ret = copy(vm, vm->ret);

143133 vm->reg1 = copy(vm, vm->reg1);

144134

@@ -150,7 +140,6 @@ void idris_gc(VM* vm) {

150140 if ((vm->heap.next - vm->heap.heap) > vm->heap.size >> 1) {

151141 vm->heap.size += vm->heap.growth;

152142 }

153− vm->heap.old = oldheap;

154143

155144 STATS_LEAVE_GC(vm->stats, vm->heap.size, vm->heap.next - vm->heap.heap)

156145 HEAP_CHECK(vm)

rts/idris_heap.c+6−3

@@ -5,7 +5,9 @@

55#include <stddef.h>

66#include <stdio.h>

77

8−void alloc_heap(Heap * h, size_t heap_size)

8+

9+/* Used for initializing the heap. */

10+void alloc_heap(Heap * h, size_t heap_size, size_t growth, char * old)

911{

1012 char * mem = malloc(heap_size);

1113 if (mem == NULL) {

@@ -27,9 +29,9 @@ void alloc_heap(Heap * h, size_t heap_size)

2729 h->end = h->heap + heap_size;

2830

2931 h->size = heap_size;

30− h->growth = heap_size;

32+ h->growth = growth;

3133

32− h->old = NULL;

34+ h->old = old;

3335}

3436

3537void free_heap(Heap * h) {

@@ -40,6 +42,7 @@ void free_heap(Heap * h) {

4042 }

4143}

4244

45+

4346// TODO: more testing

4447/******************** Heap testing ********************************************/

4548void heap_check_underflow(Heap * heap) {

rts/idris_heap.h+1−1

@@ -14,7 +14,7 @@ typedef struct {

1414} Heap;

1515

1616

17−void alloc_heap(Heap * heap, size_t heap_size);

17+void alloc_heap(Heap * heap, size_t heap_size, size_t growth, char * old);

1818void free_heap(Heap * heap);

1919

2020

rts/idris_rts.c+1−1

@@ -29,7 +29,7 @@ VM* init_vm(int stack_size, size_t heap_size,

2929 vm->valstack_base = valstack;

3030 vm->stack_max = valstack + stack_size;

3131

32− alloc_heap(&(vm->heap), heap_size);

32+ alloc_heap(&(vm->heap), heap_size, heap_size, NULL);

3333

3434 vm->ret = NULL;

3535 vm->reg1 = NULL;

src/Idris/AbsSyntax.hs+28−18

@@ -1481,31 +1481,34 @@ implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $

14811481

14821482-- Add implicit arguments in function calls

14831483addImplPat :: IState -> PTerm -> PTerm

1484−addImplPat = addImpl' True [] []

1484+addImplPat = addImpl' True [] [] []

14851485

14861486addImplBound :: IState -> [Name] -> PTerm -> PTerm

1487−addImplBound ist ns = addImpl' False ns [] ist

1487+addImplBound ist ns = addImpl' False ns [] [] ist

14881488

14891489addImplBoundInf :: IState -> [Name] -> [Name] -> PTerm -> PTerm

1490−addImplBoundInf ist ns inf = addImpl' False ns inf ist

1490+addImplBoundInf ist ns inf = addImpl' False ns inf [] ist

14911491

14921492-- | Add the implicit arguments to applications in the term

1493−addImpl :: IState -> PTerm -> PTerm

1493+-- [Name] gives the names to always expend, even when under a binder of

1494+-- that name (this is to expand methods with implicit arguments in dependent

1495+-- type classes).

1496+addImpl :: [Name] -> IState -> PTerm -> PTerm

14941497addImpl = addImpl' False [] []

14951498

14961499-- TODO: in patterns, don't add implicits to function names guarded by constructors

14971500-- and *not* inside a PHidden

14981501

1499−addImpl' :: Bool -> [Name] -> [Name] -> IState -> PTerm -> PTerm

1500−addImpl' inpat env infns ist ptm

1502+addImpl' :: Bool -> [Name] -> [Name] -> [Name] -> IState -> PTerm -> PTerm

1503+addImpl' inpat env infns imp_meths ist ptm

15011504 = mkUniqueNames env (ai False (zip env (repeat Nothing)) [] ptm)

15021505 where

15031506 ai :: Bool -> [(Name, Maybe PTerm)] -> [[T.Text]] -> PTerm -> PTerm

15041507 ai qq env ds (PRef fc f)

15051508 | f `elem` infns = PInferRef fc f

1506− | not (f `elem` map fst env) = handleErr $ aiFn inpat inpat qq ist fc f ds []

1509+ | not (f `elem` map fst env) = handleErr $ aiFn inpat inpat qq imp_meths ist fc f ds []

15071510 ai qq env ds (PHidden (PRef fc f))

1508− | not (f `elem` map fst env) = PHidden (handleErr $ aiFn inpat False qq ist fc f ds [])

1511+ | not (f `elem` map fst env) = PHidden (handleErr $ aiFn inpat False qq imp_meths ist fc f ds [])

15091512 ai qq env ds (PEq fc lt rt l r)

15101513 = let lt' = ai qq env ds lt

15111514 rt' = ai qq env ds rt

@@ -1541,7 +1544,7 @@ addImpl' inpat env infns ist ptm

15411544 | f `elem` infns = ai qq env ds (PApp fc (PInferRef fc f) as)

15421545 | not (f `elem` map fst env)

15431546 = let as' = map (fmap (ai qq env ds)) as in

1544− handleErr $ aiFn inpat False qq ist fc f ds as'

1547+ handleErr $ aiFn inpat False qq imp_meths ist fc f ds as'

15451548 | Just (Just ty) <- lookup f env =

15461549 let as' = map (fmap (ai qq env ds)) as

15471550 arity = getPArity ty in

@@ -1576,7 +1579,9 @@ addImpl' inpat env infns ist ptm

15761579 _ -> ai qq env ds (PCase fc val [(PRef fc n, sc)])

15771580 ai qq env ds (PPi p n ty sc)

15781581 = let ty' = ai qq env ds ty

1579− sc' = ai qq ((n, Just ty):env) ds sc in

1582+ env' = if n `elem` imp_meths then env

1583+ else ((n, Just ty) : env)

1584+ sc' = ai qq env' ds sc in

15801585 PPi p n ty' sc'

15811586 ai qq env ds (PGoal fc r n sc)

15821587 = let r' = ai qq env ds r

@@ -1600,8 +1605,8 @@ addImpl' inpat env infns ist ptm

16001605-- if in a pattern, and there are no arguments, and there's no possible

16011606-- names with zero explicit arguments, don't add implicits.

16021607

1603−aiFn :: Bool -> Bool -> Bool -> IState -> FC -> Name -> [[T.Text]] -> [PArg] -> Either Err PTerm

1604−aiFn inpat True qq ist fc f ds []

1608+aiFn :: Bool -> Bool -> Bool -> [Name] -> IState -> FC -> Name -> [[T.Text]] -> [PArg] -> Either Err PTerm

1609+aiFn inpat True qq imp_meths ist fc f ds []

16051610 = case lookupDef f (tt_ctxt ist) of

16061611 [] -> Right $ PPatvar fc f

16071612 alts -> let ialts = lookupCtxtName f (idris_implicits ist) in

@@ -1609,7 +1614,7 @@ aiFn inpat True qq ist fc f ds []

16091614 if (not (vname f) || tcname f

16101615 || any (conCaf (tt_ctxt ist)) ialts)

16111616-- any constructor alts || any allImp ialts))

1612− then aiFn inpat False qq ist fc f ds [] -- use it as a constructor

1617+ then aiFn inpat False qq imp_meths ist fc f ds [] -- use it as a constructor

16131618 else Right $ PPatvar fc f

16141619 where imp (PExp _ _ _ _) = False

16151620 imp _ = True

@@ -1623,9 +1628,9 @@ aiFn inpat True qq ist fc f ds []

16231628 vname (UN n) = True -- non qualified

16241629 vname _ = False

16251630

1626−aiFn inpat expat qq ist fc f ds as

1631+aiFn inpat expat qq imp_meths ist fc f ds as

16271632 | f `elem` primNames = Right $ PApp fc (PRef fc f) as

1628−aiFn inpat expat qq ist fc f ds as

1633+aiFn inpat expat qq imp_meths ist fc f ds as

16291634 -- This is where namespaces get resolved by adding PAlternative

16301635 = do let ns = lookupCtxtName f (idris_implicits ist)

16311636 let nh = filter (\(n, _) -> notHidden n) ns

@@ -1633,15 +1638,20 @@ aiFn inpat expat qq ist fc f ds as

16331638 [] -> nh

16341639 x -> x

16351640 case ns' of

1636− [(f',ns)] -> Right $ mkPApp fc (length ns) (PRef fc f') (insertImpl ns as)

1641+ [(f',ns)] -> Right $ mkPApp fc (length ns) (PRef fc (isImpName f f')) (insertImpl ns as)

16371642 [] -> if f `elem` (map fst (idris_metavars ist))

16381643 then Right $ PApp fc (PRef fc f) as

16391644 else Right $ mkPApp fc (length as) (PRef fc f) as

16401645 alts -> Right $

16411646 PAlternative True $

1642− map (\(f', ns) -> mkPApp fc (length ns) (PRef fc f')

1647+ map (\(f', ns) -> mkPApp fc (length ns) (PRef fc (isImpName f f'))

16431648 (insertImpl ns as)) alts

16441649 where

1650+ -- if the name is in imp_meths, we should actually refer to the bound

1651+ -- name rather than the global one after expanding implicits

1652+ isImpName f f' | f `elem` imp_meths = f

1653+ | otherwise = f'

1654+

16451655 trimAlts [] alts = alts

16461656 trimAlts ns alts

16471657 = filter (\(x, _) -> any (\d -> d `isPrefixOf` nspace x) ns) alts

@@ -1685,7 +1695,7 @@ aiFn inpat expat qq ist fc f ds as

16851695 PImp p True l n Placeholder :

16861696 insImpAcc (M.insert n Placeholder pnas) ps given imps

16871697 insImpAcc pnas (PTacImplicit p l n sc' ty : ps) given imps =

1688− let sc = addImpl ist (substMatches (M.toList pnas) sc') in

1698+ let sc = addImpl imp_meths ist (substMatches (M.toList pnas) sc') in

16891699 case find n imps [] of

16901700 Just (tm, imps') ->

16911701 PTacImplicit p l n sc tm :

src/Idris/AbsSyntaxTree.hs+4−1

@@ -1198,6 +1198,9 @@ data SyntaxInfo = Syn { using :: [Using],

11981198 syn_params :: [(Name, PTerm)],

11991199 syn_namespace :: [String],

12001200 no_imp :: [Name],

1201+ imp_methods :: [Name], -- class methods. When expanding

1202+ -- implicits, these should be expanded even under

1203+ -- binders

12011204 decoration :: Name -> Name,

12021205 inPattern :: Bool,

12031206 implicitAllowed :: Bool,

@@ -1211,7 +1214,7 @@ deriving instance NFData SyntaxInfo

12111214deriving instance Binary SyntaxInfo

12121215!-}

12131216

1214−defaultSyntax = Syn [] [] [] [] id False False Nothing 0 initDSL 0

1217+defaultSyntax = Syn [] [] [] [] [] id False False Nothing 0 initDSL 0

12151218

12161219expandNS :: SyntaxInfo -> Name -> Name

12171220expandNS syn n@(NS _ _) = n

src/Idris/Core/Binary.hs+6

@@ -149,6 +149,9 @@ instance Binary a => Binary (Err' a) where

149149 put (NoEliminator s t) = do putWord8 37

150150 put s

151151 put t

152+ put (InvalidTCArg n t) = do putWord8 38

153+ put n

154+ put t

152155

153156 get = do i <- getWord8

154157 case i of

@@ -211,6 +214,9 @@ instance Binary a => Binary (Err' a) where

211214 37 -> do x1 <- get

212215 x2 <- get

213216 return (NoEliminator x1 x2)

217+ 38 -> do x1 <- get

218+ x2 <- get

219+ return (InvalidTCArg x1 x2)

214220 _ -> error "Corrupted binary data for Err'"

215221----- Generated by 'derive'

216222

src/Idris/Core/DeepSeq.hs+1

@@ -81,6 +81,7 @@ instance NFData Err where

8181 rnf (NotInjective x1 x2 x3)

8282 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

8383 rnf (CantResolve x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

84+ rnf (InvalidTCArg x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

8485 rnf (CantResolveAlts x1) = rnf x1 `seq` ()

8586 rnf (IncompleteTerm x1) = rnf x1 `seq` ()

8687 rnf (NoEliminator x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

src/Idris/Core/TT.hs+27−10

@@ -157,6 +157,7 @@ data Err' t

157157 | NotInjective t t t

158158 | CantResolve Bool -- True if postponed, False if fatal

159159 t

160+ | InvalidTCArg Name t

160161 | CantResolveAlts [Name]

161162 | IncompleteTerm t

162163 | NoEliminator String t

@@ -1170,17 +1171,33 @@ unList tm = case unApply tm of

11701171forget :: TT Name -> Raw

11711172forget tm = forgetEnv [] tm

11721173

1174+safeForget :: TT Name -> Maybe Raw

1175+safeForget tm = safeForgetEnv [] tm

1176+

11731177forgetEnv :: [Name] -> TT Name -> Raw

1174−forgetEnv env (P _ n _) = Var n

1175−forgetEnv env (V i) = Var (env !! i)

1176−forgetEnv env (Bind n b sc) = let n' = uniqueName n env in

1177− RBind n' (fmap (forgetEnv env) b)

1178− (forgetEnv (n':env) sc)

1179−forgetEnv env (App f a) = RApp (forgetEnv env f) (forgetEnv env a)

1180−forgetEnv env (Constant c) = RConstant c

1181−forgetEnv env (TType i) = RType

1182−forgetEnv env (UType u) = RUType u

1183−forgetEnv env Erased = RConstant Forgot

1178+forgetEnv env tm = case safeForgetEnv env tm of

1179+ Just t' -> t'

1180+ Nothing -> error $ "Scope error in " ++ show tm

1181+

1182+

1183+safeForgetEnv :: [Name] -> TT Name -> Maybe Raw

1184+safeForgetEnv env (P _ n _) = Just $ Var n

1185+safeForgetEnv env (V i) | i < length env = Just $ Var (env !! i)

1186+ | otherwise = Nothing

1187+safeForgetEnv env (Bind n b sc)

1188+ = do let n' = uniqueName n env

1189+ b' <- safeForgetEnvB env b

1190+ sc' <- safeForgetEnv (n':env) sc

1191+ Just $ RBind n' b' sc'

1192+ where safeForgetEnvB env (Let t v) = liftM2 Let (safeForgetEnv env t)

1193+ (safeForgetEnv env v)

1194+ safeForgetEnvB env b = do ty' <- safeForgetEnv env (binderTy b)

1195+ Just $ fmap (\_ -> ty') b

1196+safeForgetEnv env (App f a) = liftM2 RApp (safeForgetEnv env f) (safeForgetEnv env a)

1197+safeForgetEnv env (Constant c) = Just $ RConstant c

1198+safeForgetEnv env (TType i) = Just RType

1199+safeForgetEnv env (UType u) = Just $ RUType u

1200+safeForgetEnv env Erased = Just $ RConstant Forgot

11841201

11851202-- | Introduce a 'Bind' into the given term for each element of the

11861203-- given list of (name, binder) pairs.

src/Idris/Coverage.hs+1−1

@@ -24,7 +24,7 @@ import Control.Monad.State.Strict

2424-- provided explicitly from new clause generation.

2525mkPatTm :: PTerm -> Idris Term

2626mkPatTm t = do i <- getIState

27− let timp = addImpl' True [] [] i t

27+ let timp = addImpl' True [] [] [] i t

2828 evalStateT (toTT (mapPT deNS timp)) 0

2929 where

3030 toTT (PRef _ n) = do i <- lift getIState

src/Idris/DeepSeq.hs+2−2

@@ -353,10 +353,10 @@ instance NFData Using where

353353 rnf (UConstraint x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

354354

355355instance NFData SyntaxInfo where

356− rnf (Syn x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11)

356+ rnf (Syn x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12)

357357 = rnf x1 `seq`

358358 rnf x2 `seq`

359359 rnf x3 `seq`

360360 rnf x4 `seq`

361361 rnf x5 `seq`

362− rnf x6 `seq` rnf x7 `seq` rnf x8 `seq` rnf x9 `seq` rnf x10 `seq` rnf x11 `seq` ()

362+ rnf x6 `seq` rnf x7 `seq` rnf x8 `seq` rnf x9 `seq` rnf x10 `seq` rnf x11 `seq` rnf x12 `seq` ()

src/Idris/Delaborate.hs+4

@@ -290,6 +290,10 @@ pprintErr' i (NotInjective p x y) =

290290 text " when unifying" <+> annTm x (pprintTerm i (delab i x)) <+> text "and" <+>

291291 annTm y (pprintTerm i (delab i y))

292292pprintErr' i (CantResolve _ c) = text "Can't resolve type class" <+> pprintTerm i (delab i c)

293+pprintErr' i (InvalidTCArg n t)

294+ = annTm t (pprintTerm i (delab i t)) <+> text " cannot be a parameter of "

295+ <> annName n <$>

296+ text "(Type class arguments must be injective)"

293297pprintErr' i (CantResolveAlts as) = text "Can't disambiguate name:" <+>

294298 align (cat (punctuate (comma <> space) (map (fmap (fancifyAnnots i) . annName) as)))

295299pprintErr' i (NoTypeDecl n) = text "No type declaration for" <+> annName n

src/Idris/Elab/Class.hs+11−11

@@ -77,28 +77,28 @@ elabClass info syn_in doc fc constraints tn ps pDocs fds ds

7777 = unzip (map (\ ( x,y,z) -> (x, y)) ims)

7878 let defaults = map (\ (x, (y, z)) -> (x,y)) defs

7979 -- build instance constructor type

80− -- decorate names of functions to ensure they can't be referred

81− -- to elsewhere in the class declaration

8280 let cty = impbind ps $ conbind constraints

8381 $ pibind (map (\ (n, ty) -> (nsroot n, ty)) methods)

8482 constraint

8583 let cons = [(emptyDocstring, [], cn, cty, fc, [])]

8684 let ddecl = PDatadecl tn tty cons

8785 logLvl 5 $ "Class data " ++ show (showDImp verbosePPOption ddecl)

88− elabData info (syn { no_imp = no_imp syn ++ mnames }) doc pDocs fc [] ddecl

89−

86+ -- Elaborate the data declaration

87+ elabData info (syn { no_imp = no_imp syn ++ mnames,

88+ imp_methods = mnames }) doc pDocs fc [] ddecl

9089 dets <- findDets cn fds

9190 addClass tn (CI cn (map nodoc imethods) defaults idecls (map fst ps) [] dets)

91+

9292 -- for each constraint, build a top level function to chase it

93− logLvl 5 $ "Building functions"

94−-- let usyn = syn { using = map (\ (x,y) -> UImplicit x y) ps

95−-- ++ using syn }

96− fns <- mapM (cfun cn constraint syn (map fst imethods)) constraints

97− mapM_ (rec_elabDecl info EAll info) (concat fns)

93+ cfns <- mapM (cfun cn constraint syn (map fst imethods)) constraints

94+ mapM_ (rec_elabDecl info EAll info) (concat cfns)

95+

9896 -- for each method, build a top level function

9997 fns <- mapM (tfun cn constraint syn (map fst imethods)) imethods

10098 logLvl 5 $ "Functions " ++ show fns

99+ -- Elaborate the the top level methods

101100 mapM_ (rec_elabDecl info EAll info) (concat fns)

101+

102102 -- add the default definitions

103103 mapM_ (rec_elabDecl info EAll info) (concat (map (snd.snd) defs))

104104 addIBC (IBCClass tn)

@@ -134,8 +134,8 @@ elabClass info syn_in doc fc constraints tn ps pDocs fds ds

134134

135135 getMName (PTy _ _ _ _ _ n _) = nsroot n

136136 tdecl allmeths (PTy doc _ syn _ o n t)

137− = do t' <- implicit' info syn allmeths n t

138− logLvl 5 $ "Method " ++ show n ++ " : " ++ showTmImpls t'

137+ = do t' <- implicit' info syn (map fst ps ++ allmeths) n t

138+ logLvl 2 $ "Method " ++ show n ++ " : " ++ showTmImpls t'

139139 return ( (n, (toExp (map fst ps) Exp t')),

140140 (n, (doc, o, (toExp (map fst ps)

141141 (\ l s p -> Imp l s p Nothing) t'))),

src/Idris/Elab/Clause.hs+10−10

@@ -548,7 +548,7 @@ elabClause :: ElabInfo -> FnOpts -> (Int, PClause) ->

548548elabClause info opts (_, PClause fc fname lhs_in [] PImpossible [])

549549 = do let tcgen = Dictionary `elem` opts

550550 i <- get

551− let lhs = addImpl i lhs_in

551+ let lhs = addImpl [] i lhs_in

552552 b <- checkPossible info fc tcgen fname lhs_in

553553 case b of

554554 True -> tclift $ tfail (At fc

@@ -603,7 +603,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc

603603 -- If we're inferring metavariables in the type, don't recheck,

604604 -- because we're only doing this to try to work out those metavariables

605605 (clhs_c, clhsty) <- if not inf

606− then recheckC fc [] lhs_tm

606+ then recheckC fc id [] lhs_tm

607607 else return (lhs_tm, lhs_ty)

608608 let clhs = normalise ctxt [] clhs_c

609609 let borrowed = borrowedNames [] clhs

@@ -681,7 +681,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc

681681 logLvl 4 $ "---> " ++ show rhs'

682682 when (not (null defer)) $ iLOG $ "DEFERRED " ++

683683 show (map (\ (n, (_,_,t)) -> (n, t)) defer)

684− def' <- checkDef fc defer

684+ def' <- checkDef fc (Elaborating "deferred type of ") defer

685685 let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, False))) def'

686686 addDeferred def''

687687 mapM_ (\(n, _) -> addIBC (IBCDef n)) def''

@@ -700,7 +700,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc

700700 logLvl 6 $ " ==> " ++ show (forget rhs')

701701

702702 (crhs, crhsty) <- if not inf

703− then recheckC_borrowing True borrowed fc [] rhs'

703+ then recheckC_borrowing True borrowed fc id [] rhs'

704704 else return (rhs', clhsty)

705705 logLvl 6 $ " ==> " ++ show crhsty ++ " against " ++ show clhsty

706706 ctxt <- getContext

@@ -828,7 +828,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)

828828 let ret_ty = getRetTy (explicitNames (normalise ctxt [] lhs_ty))

829829 let static_names = getStaticNames i lhs_tm

830830 logLvl 5 (show lhs_tm ++ "\n" ++ show static_names)

831− (clhs, clhsty) <- recheckC fc [] lhs_tm

831+ (clhs, clhsty) <- recheckC fc id [] lhs_tm

832832 logLvl 5 ("Checked " ++ show clhs)

833833 let bargs = getPBtys (explicitNames (normalise ctxt [] lhs_tm))

834834 let wval = addImplBound i (map fst bargs) wval_in

@@ -847,12 +847,12 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)

847847 return (tt, d, is, ctxt', newDecls))

848848 setContext ctxt'

849849 processTacticDecls newDecls

850− def' <- checkDef fc defer

850+ def' <- checkDef fc iderr defer

851851 let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, False))) def'

852852 addDeferred def''

853853 mapM_ (elabCaseBlock info opts) is

854854 logLvl 5 ("Checked wval " ++ show wval')

855− (cwval, cwvalty) <- recheckC fc [] (getInferTerm wval')

855+ (cwval, cwvalty) <- recheckC fc id [] (getInferTerm wval')

856856 let cwvaltyN = explicitNames (normalise ctxt [] cwvalty)

857857 let cwvalN = explicitNames (normalise ctxt [] cwval)

858858 logLvl 3 ("With type " ++ show cwvalty ++ "\nRet type " ++ show ret_ty)

@@ -907,7 +907,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)

907907 addIBC (IBCImp wname)

908908 addIBC (IBCStatic wname)

909909

910− def' <- checkDef fc [(wname, (-1, Nothing, wtype))]

910+ def' <- checkDef fc iderr [(wname, (-1, Nothing, wtype))]

911911 let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, False))) def'

912912 addDeferred def''

913913

@@ -943,12 +943,12 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)

943943 setContext ctxt'

944944 processTacticDecls newDecls

945945

946− def' <- checkDef fc defer

946+ def' <- checkDef fc iderr defer

947947 let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, False))) def'

948948 addDeferred def''

949949 mapM_ (elabCaseBlock info opts) is

950950 logLvl 5 ("Checked RHS " ++ show rhs')

951− (crhs, crhsty) <- recheckC fc [] rhs'

951+ (crhs, crhsty) <- recheckC fc id [] rhs'

952952 return $ (Right (clhs, crhs), lhs)

953953 where

954954 getImps (Bind n (Pi _ _ _) t) = pexp Placeholder : getImps t

src/Idris/Elab/Data.hs+2−1

@@ -215,6 +215,7 @@ elabCon :: ElabInfo -> SyntaxInfo -> Name -> Bool ->

215215 Idris (Name, Type)

216216elabCon info syn tn codata expkind (doc, argDocs, n, t_in, fc, forcenames)

217217 = do checkUndefined fc n

218+ logLvl 2 $ show fc ++ ":Constructor " ++ show n ++ " : " ++ show t_in

218219 (cty, ckind, t, inacc) <- buildType info syn fc [Constructor] n (if codata then mkLazy t_in else t_in)

219220 ctxt <- getContext

220221 let cty' = normalise ctxt [] cty

@@ -223,7 +224,7 @@ elabCon info syn tn codata expkind (doc, argDocs, n, t_in, fc, forcenames)

223224 -- Check that the constructor type is, in fact, a part of the family being defined

224225 tyIs n cty'

225226

226− logLvl 2 $ show fc ++ ":Constructor " ++ show n ++ " : " ++ show t

227+ logLvl 5 $ show fc ++ ":Constructor " ++ show n ++ " elaborated : " ++ show t

227228 logLvl 5 $ "Inaccessible args: " ++ show inacc

228229 logLvl 2 $ "---> " ++ show n ++ " : " ++ show cty'

229230

src/Idris/Elab/Instance.hs+29−2

@@ -135,6 +135,8 @@ elabInstance info syn doc argDocs what fc cs n ps t expn ds = do

135135 [PClause fc iname lhs [] rhs wb]]

136136 iLOG (show idecls)

137137 mapM_ (rec_elabDecl info EAll info) idecls

138+ ist <- getIState

139+ checkInjectiveArgs fc n (class_determiners ci) (lookupTyExact iname (tt_ctxt ist))

138140 addIBC (IBCInstance intInst n iname)

139141

140142 where

@@ -167,7 +169,7 @@ elabInstance info syn doc argDocs what fc cs n ps t expn ds = do

167169 = do ty' <- addUsingConstraints syn fc t

168170 -- TODO think: something more in info?

169171 ty' <- implicit info syn iname ty'

170− let ty = addImpl i ty'

172+ let ty = addImpl [] i ty'

171173 ctxt <- getContext

172174 (ElabResult tyT _ _ ctxt' newDecls, _) <-

173175 tclift $ elaborate ctxt iname (TType (UVal 0)) initEState

@@ -175,7 +177,7 @@ elabInstance info syn doc argDocs what fc cs n ps t expn ds = do

175177 setContext ctxt'

176178 processTacticDecls newDecls

177179 ctxt <- getContext

178− (cty, _) <- recheckC fc [] tyT

180+ (cty, _) <- recheckC fc id [] tyT

179181 let nty = normalise ctxt [] cty

180182 return $ any (isJust . findOverlapping i (class_determiners ci) (delab i nty)) (class_instances ci)

181183

@@ -276,3 +278,28 @@ elabInstance info syn doc argDocs what fc cs n ps t expn ds = do

276278 clauseFor m iname ns (PClauses _ _ m' _)

277279 = decorate ns iname m == decorate ns iname m'

278280 clauseFor m iname ns _ = False

281+

282+checkInjectiveArgs :: FC -> Name -> [Int] -> Maybe Type -> Idris ()

283+checkInjectiveArgs fc n ds Nothing = return ()

284+checkInjectiveArgs fc n ds (Just ty)

285+ = do ist <- getIState

286+ let (_, args) = unApply (instantiateRetTy ty)

287+ ci 0 ist args

288+ where

289+ ci i ist (a : as) | i `elem` ds

290+ = if isInj ist a then ci (i + 1) ist as

291+ else tclift $ tfail (At fc (InvalidTCArg n a))

292+ ci i ist (a : as) = ci (i + 1) ist as

293+ ci i ist [] = return ()

294+

295+ isInj i (P Bound n _) = True

296+ isInj i (P _ n _) = isConName n (tt_ctxt i)

297+ isInj i (App f a) = isInj i f && isInj i a

298+ isInj i (V _) = True

299+ isInj i (Bind n b sc) = isInj i sc

300+ isInj _ _ = True

301+

302+ instantiateRetTy (Bind n (Pi _ _ _) sc)

303+ = substV (P Bound n Erased) (instantiateRetTy sc)

304+ instantiateRetTy t = t

305+

src/Idris/Elab/Transform.hs+2−2

@@ -63,7 +63,7 @@ elabTransform info fc safe lhs_in@(PApp _ (PRef _ tf) _) rhs_in

6363 let lhs_ty = getInferType lhs'

6464 let newargs = pvars i lhs_tm

6565

66− (clhs_tm_in, clhs_ty) <- recheckC fc [] lhs_tm

66+ (clhs_tm_in, clhs_ty) <- recheckC fc id [] lhs_tm

6767 let clhs_tm = renamepats pnames clhs_tm_in

6868 logLvl 3 ("Transform LHS " ++ show clhs_tm)

6969

@@ -80,7 +80,7 @@ elabTransform info fc safe lhs_in@(PApp _ (PRef _ tf) _) rhs_in

8080 setContext ctxt'

8181 processTacticDecls newDecls

8282

83− (crhs_tm_in, crhs_ty) <- recheckC fc [] rhs'

83+ (crhs_tm_in, crhs_ty) <- recheckC fc id [] rhs'

8484 let crhs_tm = renamepats pnames crhs_tm_in

8585 logLvl 3 ("Transform RHS " ++ show crhs_tm)

8686

src/Idris/Elab/Type.hs+7−7

@@ -57,13 +57,13 @@ buildType info syn fc opts n ty' = do

5757 ctxt <- getContext

5858 i <- getIState

5959

60− logLvl 3 $ show n ++ " pre-type " ++ showTmImpls ty'

60+ logLvl 2 $ show n ++ " pre-type " ++ showTmImpls ty' ++ show (no_imp syn)

6161 ty' <- addUsingConstraints syn fc ty'

6262 ty' <- addUsingImpls syn n fc ty'

63− let ty = addImpl i ty'

63+ let ty = addImpl (imp_methods syn) i ty'

6464

65− logLvl 3 $ show n ++ " type pre-addimpl " ++ showTmImpls ty'

66− logLvl 3 $ show n ++ " type " ++ show (using syn) ++ "\n" ++ showTmImpls ty

65+ logLvl 5 $ show n ++ " type pre-addimpl " ++ showTmImpls ty'

66+ logLvl 2 $ show n ++ " type " ++ show (using syn) ++ "\n" ++ showTmImpls ty

6767

6868 (ElabResult tyT' defer is ctxt' newDecls, log) <-

6969 tclift $ elaborate ctxt n (TType (UVal 0)) initEState

@@ -75,7 +75,7 @@ buildType info syn fc opts n ty' = do

7575

7676 logLvl 3 $ show ty ++ "\nElaborated: " ++ show tyT'

7777

78− ds <- checkAddDef True False fc defer

78+ ds <- checkAddDef True False fc iderr defer

7979 -- if the type is not complete, note that we'll need to infer

8080 -- things later (for solving metavariables)

8181 when (not (null ds)) $ addTyInferred n

@@ -85,7 +85,7 @@ buildType info syn fc opts n ty' = do

8585 logLvl 5 $ "Rechecking"

8686 logLvl 6 $ show tyT

8787 logLvl 10 $ "Elaborated to " ++ showEnvDbg [] tyT

88− (cty, ckind) <- recheckC fc [] tyT

88+ (cty, ckind) <- recheckC fc id [] tyT

8989

9090 -- record the implicit and inaccessible arguments

9191 i <- getIState

@@ -154,7 +154,7 @@ elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params

154154 -- Productivity checking now via checking for guarded 'Delay'

155155 let opts' = opts -- if corec then (Coinductive : opts) else opts

156156 let usety = if norm then nty' else nty

157− ds <- checkDef fc [(n, (-1, Nothing, usety))]

157+ ds <- checkDef fc iderr [(n, (-1, Nothing, usety))]

158158 addIBC (IBCDef n)

159159 let ds' = map (\(n, (i, top, t)) -> (n, (i, top, t, True))) ds

160160 addDeferred ds'

src/Idris/Elab/Utils.hs+16−10

@@ -24,30 +24,36 @@ import qualified Data.Map as Map

2424

2525recheckC = recheckC_borrowing False []

2626

27−recheckC_borrowing uniq_check bs fc env t

27+recheckC_borrowing uniq_check bs fc mkerr env t

2828 = do -- t' <- applyOpts (forget t) (doesn't work, or speed things up...)

2929 ctxt <- getContext

30− (tm, ty, cs) <- tclift $ case recheck_borrowing uniq_check bs ctxt env (forget t) t of

31− Error e -> tfail (At fc e)

30+ t' <- case safeForget t of

31+ Just ft -> return ft

32+ Nothing -> tclift $ tfail $ mkerr (At fc (IncompleteTerm t))

33+ (tm, ty, cs) <- tclift $ case recheck_borrowing uniq_check bs ctxt env t' t of

34+ Error e -> tfail (At fc (mkerr e))

3235 OK x -> return x

3336 logLvl 6 $ "CONSTRAINTS ADDED: " ++ show cs

3437 addConstraints fc cs

3538 return (tm, ty)

3639

37−checkDef :: FC -> [(Name, (Int, Maybe Name, Type))]

40+iderr :: Name -> Err -> Err

41+iderr _ e = e

42+

43+checkDef :: FC -> (Name -> Err -> Err) -> [(Name, (Int, Maybe Name, Type))]

3844 -> Idris [(Name, (Int, Maybe Name, Type))]

39−checkDef fc ns = checkAddDef False True fc ns

45+checkDef fc mkerr ns = checkAddDef False True fc mkerr ns

4046

41−checkAddDef :: Bool -> Bool -> FC

47+checkAddDef :: Bool -> Bool -> FC -> (Name -> Err -> Err)

4248 -> [(Name, (Int, Maybe Name, Type))]

4349 -> Idris [(Name, (Int, Maybe Name, Type))]

44−checkAddDef add toplvl fc [] = return []

45−checkAddDef add toplvl fc ((n, (i, top, t)) : ns)

50+checkAddDef add toplvl fc mkerr [] = return []

51+checkAddDef add toplvl fc mkerr ((n, (i, top, t)) : ns)

4652 = do ctxt <- getContext

47− (t', _) <- recheckC fc [] t

53+ (t', _) <- recheckC fc (mkerr n) [] t

4854 when add $ do addDeferred [(n, (i, top, t, toplvl))]

4955 addIBC (IBCDef n)

50− ns' <- checkAddDef add toplvl fc ns

56+ ns' <- checkAddDef add toplvl fc mkerr ns

5157 return ((n, (i, top, t')) : ns')

5258

5359-- | Get the list of (index, name) of inaccessible arguments from an elaborated

src/Idris/Elab/Value.hs+3−3

@@ -56,7 +56,7 @@ elabValBind :: ElabInfo -> ElabMode -> Bool -> PTerm -> Idris (Term, Type, [(Nam

5656elabValBind info aspat norm tm_in

5757 = do ctxt <- getContext

5858 i <- getIState

59− let tm = addImpl i tm_in

59+ let tm = addImpl [] i tm_in

6060 logLvl 10 (showTmImpls tm)

6161 -- try:

6262 -- * ordinary elaboration

@@ -73,13 +73,13 @@ elabValBind info aspat norm tm_in

7373

7474 let vtm = orderPats (getInferTerm tm')

7575

76− def' <- checkDef (fileFC "(input)") defer

76+ def' <- checkDef (fileFC "(input)") iderr defer

7777 let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, True))) def'

7878 addDeferred def''

7979 mapM_ (elabCaseBlock info []) is

8080

8181 logLvl 3 ("Value: " ++ show vtm)

82− (vtm_in, vty) <- recheckC (fileFC "(input)") [] vtm

82+ (vtm_in, vty) <- recheckC (fileFC "(input)") id [] vtm

8383

8484 let vtm = if norm then normalise (tt_ctxt i) [] vtm_in

8585 else vtm_in

src/Idris/ElabTerm.hs+6−2

@@ -57,7 +57,7 @@ processTacticDecls info =

5757 updateIState $ \i -> i { idris_implicits =

5858 addDef n impls (idris_implicits i) }

5959 addIBC (IBCImp n)

60− ds <- checkDef fc [(n, (-1, Nothing, ty))]

60+ ds <- checkDef fc iderr [(n, (-1, Nothing, ty))]

6161 addIBC (IBCDef n)

6262 let ds' = map (\(n, (i, top, t)) -> (n, (i, top, t, True))) ds

6363 addDeferred ds'

@@ -1375,9 +1375,12 @@ findInstances :: IState -> Term -> [Name]

13751375findInstances ist t

13761376 | (P _ n _, _) <- unApply t

13771377 = case lookupCtxt n (idris_classes ist) of

1378− [CI _ _ _ _ _ ins _] -> ins

1378+ [CI _ _ _ _ _ ins _] -> filter accessible ins

13791379 _ -> []

13801380 | otherwise = []

1381+ where accessible n = case lookupDefAccExact n False (tt_ctxt ist) of

1382+ Just (_, Hidden) -> False

1383+ _ -> True

13811384

13821385-- Try again to solve auto implicits

13831386solveAuto :: IState -> Name -> Bool -> Name -> ElabD ()

@@ -2708,6 +2711,7 @@ reflectErr (NotInjective t1 t2 t3) =

27082711 , reflect t3

27092712 ]

27102713reflectErr (CantResolve _ t) = raw_apply (Var $ reflErrName "CantResolve") [reflect t]

2714+reflectErr (InvalidTCArg n t) = raw_apply (Var $ reflErrName "InvalidTCArg") [reflectName n, reflect t]

27112715reflectErr (CantResolveAlts ss) =

27122716 raw_apply (Var $ reflErrName "CantResolveAlts")

27132717 [rawList (Var $ reflm "TTName") (map reflectName ss)]

src/Idris/IBC.hs+2−2

@@ -1420,7 +1420,7 @@ instance Binary Using where

14201420 _ -> error "Corrupted binary data for Using"

14211421

14221422instance Binary SyntaxInfo where

1423− put (Syn x1 x2 x3 x4 _ x5 x6 _ _ x7 _)

1423+ put (Syn x1 x2 x3 x4 _ _ x5 x6 _ _ x7 _)

14241424 = do put x1

14251425 put x2

14261426 put x3

@@ -1436,7 +1436,7 @@ instance Binary SyntaxInfo where

14361436 x5 <- get

14371437 x6 <- get

14381438 x7 <- get

1439− return (Syn x1 x2 x3 x4 id x5 x6 Nothing 0 x7 0)

1439+ return (Syn x1 x2 x3 x4 [] id x5 x6 Nothing 0 x7 0)

14401440

14411441instance (Binary t) => Binary (PClause' t) where

14421442 put x

src/Idris/Prover.hs+1−1

@@ -78,7 +78,7 @@ prove opt ctxt lit n ty

7878 putIState (i { proof_list = (n, prf) : proofs })

7979 let tree = simpleCase False (STerm Erased) False CompileTime (fileFC "proof") [] [] [([], P Ref n ty, tm)]

8080 logLvl 3 (show tree)

81− (ptm, pty) <- recheckC (fileFC "proof") [] tm

81+ (ptm, pty) <- recheckC (fileFC "proof") id [] tm

8282 logLvl 5 ("Proof type: " ++ show pty ++ "\n" ++

8383 "Expected type:" ++ show ty)

8484 case converts ctxt [] ty pty of

src/Idris/TypeSearch.hs+1−1

@@ -46,7 +46,7 @@ searchByType pkgs pterm = do

4646 mapM_ loadPkgIndex pkgs

4747 pterm' <- addUsingConstraints syn emptyFC pterm

4848 pterm'' <- implicit toplevel syn name pterm'

49− let pterm''' = addImpl i pterm''

49+ let pterm''' = addImpl [] i pterm''

5050 ty <- elabType toplevel syn (fst noDocs) (snd noDocs) emptyFC [] name pterm'

5151 let names = searchUsing searchPred i ty

5252 let names' = take numLimit names

test/quasiquote001/expected+2−2

@@ -1,5 +1,5 @@

11(App (App (App (P (DCon 1 3) (NS (UN ::) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 2)))))) (P (TCon 8 0) (UN Unit) (TType (UVar -1)))) (P (DCon 0 0) (UN MkUnit) (P (TCon 0 0) (UN Unit) Erased))) (App (App (App (P (DCon 1 3) (NS (UN ::) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 2)))))) (P (TCon 8 0) (UN Unit) (TType (UVar -1)))) (P (DCon 0 0) (UN MkUnit) (P (TCon 0 0) (UN Unit) Erased))) (App (P (DCon 0 1) (NS (UN Nil) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 0)))) (P (TCon 8 0) (UN Unit) (TType (UVar -1))))))

22--------------

3−(App (App (App (P (DCon 1 3) (NS (UN ::) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 2)))))) (TType (UVar 48))) (TType (UVar 50))) (App (App (App (P (DCon 1 3) (NS (UN ::) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 2)))))) (TType (UVar 52))) (App (App (App (App (P (DCon 0 4) (NS (UN MkPair) ["Builtins"]) (Bind (UN A) (Pi (TType (UVar -1))) (Bind (UN B) (Pi (TType (UVar -1))) (Bind (UN a) (Pi (V 1)) (Bind (UN b) (Pi (V 1)) (App (App (P (TCon 0 0) (NS (UN Pair) ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar 42))) (TType (UVar 44))) (P (TCon 8 0) (NS (UN Nat) ["Nat", "Prelude"]) (TType (UVar -1)))) (P (TCon 8 0) (NS (UN Nat) ["Nat", "Prelude"]) (TType (UVar -1))))) (App (P (DCon 0 1) (NS (UN Nil) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 0)))) (TType (UVar 54)))))

3+(App (App (App (P (DCon 1 3) (NS (UN ::) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 2)))))) (TType (UVar 32))) (TType (UVar 34))) (App (App (App (P (DCon 1 3) (NS (UN ::) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 2)))))) (TType (UVar 36))) (App (App (App (App (P (DCon 0 4) (NS (UN MkPair) ["Builtins"]) (Bind (UN A) (Pi (TType (UVar -1))) (Bind (UN B) (Pi (TType (UVar -1))) (Bind (UN a) (Pi (V 1)) (Bind (UN b) (Pi (V 1)) (App (App (P (TCon 0 0) (NS (UN Pair) ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar 30))) (TType (UVar 32))) (P (TCon 8 0) (NS (UN Nat) ["Nat", "Prelude"]) (TType (UVar -1)))) (P (TCon 8 0) (NS (UN Nat) ["Nat", "Prelude"]) (TType (UVar -1))))) (App (P (DCon 0 1) (NS (UN Nil) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 0)))) (TType (UVar 38)))))

44--------------

5−(App (App (App (App (P (DCon 0 4) (NS (UN MkPair) ["Builtins"]) (Bind (UN A) (Pi (TType (UVar -1))) (Bind (UN B) (Pi (TType (UVar -1))) (Bind (UN a) (Pi (V 1)) (Bind (UN b) (Pi (V 1)) (App (App (P (TCon 0 0) (NS (UN Pair) ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar 42))) (TType (UVar 44))) (App (App (App (App (P (DCon 0 4) (NS (UN MkPair) ["Builtins"]) (Bind (UN A) (Pi (TType (UVar -1))) (Bind (UN B) (Pi (TType (UVar -1))) (Bind (UN a) (Pi (V 1)) (Bind (UN b) (Pi (V 1)) (App (App (P (TCon 0 0) (NS (UN Pair) ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar 42))) (TType (UVar 44))) (TType (UVar 48))) (TType (UVar 48)))) (App (App (App (App (P (DCon 0 4) (NS (UN MkPair) ["Builtins"]) (Bind (UN A) (Pi (TType (UVar -1))) (Bind (UN B) (Pi (TType (UVar -1))) (Bind (UN a) (Pi (V 1)) (Bind (UN b) (Pi (V 1)) (App (App (P (TCon 0 0) (NS (UN Pair) ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar 42))) (TType (UVar 44))) (TType (UVar 48))) (TType (UVar 48))))

5+(App (App (App (App (P (DCon 0 4) (NS (UN MkPair) ["Builtins"]) (Bind (UN A) (Pi (TType (UVar -1))) (Bind (UN B) (Pi (TType (UVar -1))) (Bind (UN a) (Pi (V 1)) (Bind (UN b) (Pi (V 1)) (App (App (P (TCon 0 0) (NS (UN Pair) ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar 30))) (TType (UVar 32))) (App (App (App (App (P (DCon 0 4) (NS (UN MkPair) ["Builtins"]) (Bind (UN A) (Pi (TType (UVar -1))) (Bind (UN B) (Pi (TType (UVar -1))) (Bind (UN a) (Pi (V 1)) (Bind (UN b) (Pi (V 1)) (App (App (P (TCon 0 0) (NS (UN Pair) ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar 30))) (TType (UVar 32))) (TType (UVar 32))) (TType (UVar 32)))) (App (App (App (App (P (DCon 0 4) (NS (UN MkPair) ["Builtins"]) (Bind (UN A) (Pi (TType (UVar -1))) (Bind (UN B) (Pi (TType (UVar -1))) (Bind (UN a) (Pi (V 1)) (Bind (UN b) (Pi (V 1)) (App (App (P (TCon 0 0) (NS (UN Pair) ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar 30))) (TType (UVar 32))) (TType (UVar 32))) (TType (UVar 32))))

test/reg059/expectednew file

No changes to the content.

test/reg059/reg059.idrnew file+8

@@ -0,0 +1,8 @@

1+class Monad m => ContainerMonad (m : Type -> Type) where

2+ Elem : a -> m a -> Type

3+ tagElem : (mx : m a) -> m (x : a ** Elem x mx)

4+

5+class Monad m => ContainerMonad2 a (m : Type -> Type) where

6+ Elem2 : a -> m a -> Type

7+ tagElem2 : (mx : m a) -> m (x : a ** Elem2 x mx)

8+

test/reg059/runnew file+3

@@ -0,0 +1,3 @@

1+#!/usr/bin/env bash

2+idris $@ reg059.idr --check

3+rm -f *.ibc

test/unique001/expected+1−1

@@ -17,4 +17,4 @@ with

1717unique001b.idr:16:7:Borrowed name xs must not be used on RHS

1818unique001c.idr:46:6:Unique name f is used more than once

1919unique001d.idr:3:7:Borrowed name x must not be used on RHS

20−unique001e.idr:4:11:Constructor Main.:: has a UniqueType, but the data type does not

20+unique001e.idr:3:10:Constructor Main.Nil has a UniqueType, but the data type does not