dbe0a3c · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Check class arguments for injectivity

We assumed this in the unifier, so if we don't check we'll get lots of strange behaviour.

commitdbe0a3c48124cbb66441e09dc5b38bf5ce0d697f authorEdwin Brady <ecb10@st-andrews.ac.uk> dateThu 19 Mar 2015, 19:28 (12 years ago) parenta281e23 446d99d

13 files changed+52−9

compare with master

unifiedsplit

CHANGELOG+2 libs/base/Language/Reflection/Utils.idr+1 libs/prelude/Language/Reflection/Errors.idr+1 libs/prelude/Prelude/Applicative.idr−4 libs/prelude/Prelude/Functor.idr−2 libs/prelude/Prelude/Monad.idr−3 rts/idris_gc.c+8 src/Idris/Core/Binary.hs+6 src/Idris/Core/DeepSeq.hs+1 src/Idris/Core/TT.hs+1 src/Idris/Delaborate.hs+4 src/Idris/Elab/Instance.hs+27 src/Idris/ElabTerm.hs+1

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

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

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

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

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

117117

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+

118126 vm->heap.heap = newheap;

119127#ifdef FORCE_ALIGNMENT

120128 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

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

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

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

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

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

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

27112711 , reflect t3

27122712 ]

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

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

27142715reflectErr (CantResolveAlts ss) =

27152716 raw_apply (Var $ reflErrName "CantResolveAlts")

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