dbe0a3c · Idris-dev · git.iko.soy

CHANGELOG+2

compare with master

unifiedsplit

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

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

41 must be available before resolving instances. Only determining parameters

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

43

45

44New in 0.9.16:

46New in 0.9.16:

45--------------

47--------------

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−

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

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

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

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

24 map g x = pure g <*> x

20 map g x = pure g <*> x

libs/prelude/Prelude/Functor.idr−2

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

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

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

26

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

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

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

26

27−instance Monad id where

28− a >>= f = f a

29−

30||| Also called `join` or mu

27||| Also called `join` or mu

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

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

32flatten a = a >>= id

29flatten a = a >>= id

rts/idris_gc.c+8

@@ -115,6 +115,14 @@ void idris_gc(VM* vm) {

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

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

117

118+ if (newheap == NULL) {

119+ fprintf(stderr,

120+ "GC ERROR: Unable to allocate new heap. Requested %zd bytes.\n",

121+ vm->heap.size);

122+

123+ exit(EXIT_FAILURE);

124+ }

125+

118 vm->heap.heap = newheap;

126 vm->heap.heap = newheap;

119#ifdef FORCE_ALIGNMENT

127#ifdef FORCE_ALIGNMENT

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

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

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+1

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

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/Instance.hs+27

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

@@ -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/ElabTerm.hs+1

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

2711 , reflect t3

2712 ]

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

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

2714reflectErr (CantResolveAlts ss) =

2715reflectErr (CantResolveAlts ss) =

2715 raw_apply (Var $ reflErrName "CantResolveAlts")

2716 raw_apply (Var $ reflErrName "CantResolveAlts")

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

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