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

CHANGELOG+2

compare with master

unifiedsplit

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

43* New package 'contrib' containing things that are less mature or less used

44 than the contents of 'base'. 'contrib' is not available by default, so you

45 may need to add '-p contrib' to your .ipkg file or Idris command line.

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

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

46

48

47New in 0.9.16:

49New in 0.9.16:

48--------------

50--------------

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

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

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

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

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

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

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

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

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

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

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

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

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

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

29 | NoTypeDecl TTName

30 | NotInjective TT TT TT

31 | CantResolve TT

32+ | InvalidTCArg TTName TT

32 | CantResolveAlts (List TTName)

33 | CantResolveAlts (List TTName)

33 | IncompleteTerm TT

34 | IncompleteTerm TT

34 | NoEliminator String TT

35 | NoEliminator String TT

libs/prelude/Prelude/Applicative.idr−4

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

15 pure : a -> f a

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

17

18−instance Applicative id where

19− pure a = a

20− f <*> a = f a

21−

22infixl 2 <*

18infixl 2 <*

23(<*) : Applicative f => f a -> f b -> f a

19(<*) : Applicative f => f a -> f b -> f a

24a <* b = map const a <*> b

20a <* b = map const a <*> b

libs/prelude/Prelude/Functor.idr−2

@@ -18,5 +18,3 @@ infixl 4 <$>

18(<$>) : Functor f => (m : a -> b) -> f a -> f b

19m <$> x = map m x

20

21−instance Functor id where

22− map f a = f a

libs/prelude/Prelude/Monad.idr−3

@@ -14,9 +14,6 @@ infixl 5 >>=

14class Applicative m => Monad (m : Type -> Type) where

15 (>>=) : m a -> (a -> m b) -> m b

16

17−instance Monad id where

18− a >>= f = f a

19−

20||| Also called `join` or mu

17||| Also called `join` or mu

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

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

22flatten a = a >>= id

19flatten a = a >>= id

rts/idris_gc.c+3−14

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

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

113 free(vm->heap.old);

114

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

115+ /* Allocate swap heap. */

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

116+ alloc_heap(&vm->heap, vm->heap.size, vm->heap.growth, 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;

128

117

129 VAL* root;

118 VAL* root;

130

119

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

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

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

140 }

129 }

141#endif

130#endif

131+

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

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

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

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

144

134

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

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

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

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

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

152 }

142 }

153− vm->heap.old = oldheap;

154

143

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

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

156 HEAP_CHECK(vm)

145 HEAP_CHECK(vm)

rts/idris_heap.c+6−3

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

5#include <stddef.h>

6#include <stdio.h>

7

8+

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

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

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

9{

11{

10 char * mem = malloc(heap_size);

12 char * mem = malloc(heap_size);

11 if (mem == NULL) {

13 if (mem == NULL) {

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

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

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

28

30

29 h->size = heap_size;

31 h->size = heap_size;

30− h->growth = heap_size;

32+ h->growth = growth;

31

33

32− h->old = NULL;

34+ h->old = old;

33}

35}

34

36

35void free_heap(Heap * h) {

37void free_heap(Heap * h) {

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

40 }

42 }

41}

43}

42

44

45+

43// TODO: more testing

46// TODO: more testing

44/******************** Heap testing ********************************************/

47/******************** Heap testing ********************************************/

45void heap_check_underflow(Heap * heap) {

48void heap_check_underflow(Heap * heap) {

rts/idris_heap.h+1−1

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

14} Heap;

15

16

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);

18void free_heap(Heap * heap);

19

20

rts/idris_rts.c+1−1

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

29 vm->valstack_base = valstack;

30 vm->stack_max = valstack + stack_size;

31

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

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

33

34 vm->ret = NULL;

35 vm->reg1 = NULL;

src/Idris/Core/Binary.hs+6

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

149 put (NoEliminator s t) = do putWord8 37

150 put s

151 put t

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

153+ put n

154+ put t

152

155

153 get = do i <- getWord8

156 get = do i <- getWord8

154 case i of

157 case i of

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

211 37 -> do x1 <- get

214 37 -> do x1 <- get

212 x2 <- get

215 x2 <- get

213 return (NoEliminator x1 x2)

216 return (NoEliminator x1 x2)

217+ 38 -> do x1 <- get

218+ x2 <- get

219+ return (InvalidTCArg x1 x2)

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

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

215----- Generated by 'derive'

221----- Generated by 'derive'

216

222

src/Idris/Core/DeepSeq.hs+1

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

81 rnf (NotInjective x1 x2 x3)

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

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

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

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

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

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

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

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

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

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

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

157 | NotInjective t t t

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

159 t

160+ | InvalidTCArg Name t

160 | CantResolveAlts [Name]

161 | CantResolveAlts [Name]

161 | IncompleteTerm t

162 | IncompleteTerm t

162 | NoEliminator String t

163 | NoEliminator String t

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

1170forget :: TT Name -> Raw

1171forget :: TT Name -> Raw

1171forget tm = forgetEnv [] tm

1172forget tm = forgetEnv [] tm

1172

1173

1174+safeForget :: TT Name -> Maybe Raw

1175+safeForget tm = safeForgetEnv [] tm

1176+

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

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

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

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

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

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

1186+ | otherwise = Nothing

1187+safeForgetEnv env (Bind n b sc)

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

1188+ = do let n' = uniqueName n env

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

1189+ b' <- safeForgetEnvB env b

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

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

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

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)

1180−forgetEnv env (Constant c) = RConstant c

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

1181−forgetEnv env (TType i) = RType

1198+safeForgetEnv env (TType i) = Just RType

1182−forgetEnv env (UType u) = RUType u

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

1183−forgetEnv env Erased = RConstant Forgot

1200+safeForgetEnv env Erased = Just $ RConstant Forgot

1184

1201

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

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

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

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

src/Idris/Delaborate.hs+4

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

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

291 annTm y (pprintTerm i (delab i y))

292pprintErr' 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)"

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

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

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

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

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

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

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

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

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

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

605 (clhs_c, clhsty) <- if not inf

606− then recheckC fc [] lhs_tm

606+ then recheckC fc id [] lhs_tm

607 else return (lhs_tm, lhs_ty)

608 let clhs = normalise ctxt [] clhs_c

609 let borrowed = borrowedNames [] clhs

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

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

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

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

684− def' <- checkDef fc defer

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

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

686 addDeferred def''

687 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

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

701

702 (crhs, crhsty) <- if not inf

703− then recheckC_borrowing True borrowed fc [] rhs'

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

704 else return (rhs', clhsty)

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

706 ctxt <- getContext

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

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

829 let static_names = getStaticNames i lhs_tm

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

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

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

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

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

834 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)

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

848 setContext ctxt'

849 processTacticDecls newDecls

850− def' <- checkDef fc defer

850+ def' <- checkDef fc iderr defer

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

852 addDeferred def''

853 mapM_ (elabCaseBlock info opts) is

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

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

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

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

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

858 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)

907 addIBC (IBCImp wname)

908 addIBC (IBCStatic wname)

909

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

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

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

912 addDeferred def''

913

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

943 setContext ctxt'

944 processTacticDecls newDecls

945

946− def' <- checkDef fc defer

946+ def' <- checkDef fc iderr defer

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

948 addDeferred def''

949 mapM_ (elabCaseBlock info opts) is

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

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

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

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

953 where

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

src/Idris/Elab/Instance.hs+28−1

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

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

136 iLOG (show idecls)

137 mapM_ (rec_elabDecl info EAll info) idecls

138+ ist <- getIState

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

138 addIBC (IBCInstance intInst n iname)

140 addIBC (IBCInstance intInst n iname)

139

141

140 where

142 where

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

175 setContext ctxt'

177 setContext ctxt'

176 processTacticDecls newDecls

178 processTacticDecls newDecls

177 ctxt <- getContext

179 ctxt <- getContext

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

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

179 let nty = normalise ctxt [] cty

181 let nty = normalise ctxt [] cty

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

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

181

183

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

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

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

277 = decorate ns iname m == decorate ns iname m'

279 = decorate ns iname m == decorate ns iname m'

278 clauseFor m iname ns _ = False

280 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

63 let lhs_ty = getInferType lhs'

64 let newargs = pvars i lhs_tm

65

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

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

67 let clhs_tm = renamepats pnames clhs_tm_in

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

69

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

80 setContext ctxt'

81 processTacticDecls newDecls

82

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

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

84 let crhs_tm = renamepats pnames crhs_tm_in

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

86

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

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

75

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

77

78− ds <- checkAddDef True False fc defer

78+ ds <- checkAddDef True False fc iderr defer

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

80 -- things later (for solving metavariables)

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

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

85 logLvl 5 $ "Rechecking"

86 logLvl 6 $ show tyT

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

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

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

89

90 -- record the implicit and inaccessible arguments

91 i <- getIState

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

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

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

156 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))]

158 addIBC (IBCDef n)

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

160 addDeferred ds'

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

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

24

25recheckC = recheckC_borrowing False []

26

27−recheckC_borrowing uniq_check bs fc env t

27+recheckC_borrowing uniq_check bs fc mkerr env t

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

29 ctxt <- getContext

30+ t' <- case safeForget t of

31+ Just ft -> return ft

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

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

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

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

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

32 OK x -> return x

35 OK x -> return x

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

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

34 addConstraints fc cs

37 addConstraints fc cs

35 return (tm, ty)

38 return (tm, ty)

36

39

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

41+iderr _ e = e

42+

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

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

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

44 -> 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

40

46

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

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

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

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

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

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

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

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

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

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

46 = do ctxt <- getContext

52 = do ctxt <- getContext

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

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

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

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

49 addIBC (IBCDef n)

55 addIBC (IBCDef n)

50− ns' <- checkAddDef add toplvl fc ns

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

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

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

52

58

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

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

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

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

73

74 let vtm = orderPats (getInferTerm tm')

75

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

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

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

78 addDeferred def''

79 mapM_ (elabCaseBlock info []) is

80

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

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

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

83

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

85 else vtm_in

src/Idris/ElabTerm.hs+6−2

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

57 updateIState $ \i -> i { idris_implicits =

58 addDef n impls (idris_implicits i) }

59 addIBC (IBCImp n)

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

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

61 addIBC (IBCDef n)

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

63 addDeferred ds'

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

1375findInstances ist t

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

1377 = case lookupCtxt n (idris_classes ist) of

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

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

1379 _ -> []

1380 | otherwise = []

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

1382+ Just (_, Hidden) -> False

1383+ _ -> True

1381

1384

1382-- Try again to solve auto implicits

1385-- Try again to solve auto implicits

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

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

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

2708 , reflect t3

2711 , reflect t3

2709 ]

2712 ]

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

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

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

2711reflectErr (CantResolveAlts ss) =

2715reflectErr (CantResolveAlts ss) =

2712 raw_apply (Var $ reflErrName "CantResolveAlts")

2716 raw_apply (Var $ reflErrName "CantResolveAlts")

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

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

src/Idris/Prover.hs+1−1

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

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

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

80 logLvl 3 (show tree)

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

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

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

83 "Expected type:" ++ show ty)

84 case converts ctxt [] ty pty of

test/quasiquote001/expected+2−2

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

1(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))))))

2--------------

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)))))

4--------------

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/unique001/expected+1−1

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

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

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

19unique001d.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