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

CHANGELOG+2

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

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

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

4545 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.

4648

4749New in 0.9.16:

4850--------------

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−

2218infixl 2 <*

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

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

libs/prelude/Prelude/Functor.idr−2

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

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

1919m <$> x = map m x

2020

21−instance Functor id where

22− map f a = f a

libs/prelude/Prelude/Monad.idr−3

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

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

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

1616

17−instance Monad id where

18− a >>= f = f a

19−

2017||| Also called `join` or mu

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

2219flatten 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/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/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/Clause.hs+9−9

@@ -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/Instance.hs+28−1

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

@@ -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+3−3

@@ -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+2−2

@@ -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/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

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