d1941f5 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Fix bug with Type*/AnyType in data decls

(Type* now deprecated and replaced with AnyType). If an AnyType is a parameter of a type, the type itself must be an AnyType otherwise we might be able to duplicate a unique thing by mistake.

commitd1941f50d3c9d710123a9529c6769522e9b8be8d authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSun 26 Apr 2015, 14:41 (11 years ago) parent84ba376

5 files changed+19−7

compare with master

unifiedsplit

src/Idris/Core/TT.hs+1−1 src/Idris/Elab/Class.hs+8−1 src/Idris/Elab/Data.hs+6−2 src/Idris/ParseExpr.hs+1 test/unique001/unique001c.idr+3−3

src/Idris/Core/TT.hs+1−1

@@ -653,7 +653,7 @@ data Universe = NullType | UniqueType | AllTypes

653653instance Show Universe where

654654 show UniqueType = "UniqueType"

655655 show NullType = "NullType"

656− show AllTypes = "Type*"

656+ show AllTypes = "AnyType"

657657

658658data Raw = Var Name

659659 | RBind Name (Binder Raw) Raw

src/Idris/Elab/Class.hs+8−1

@@ -106,7 +106,14 @@ elabClass info syn_in doc fc constraints tn ps pDocs fds ds

106106 where

107107 nodoc (n, (_, o, t)) = (n, (o, t))

108108 pibind [] x = x

109− pibind ((n, ty): ns) x = PPi expl n ty (pibind ns x)

109+ pibind ((n, ty): ns) x = PPi expl n ty (pibind ns (chkUniq ty x))

110+

111+ -- To make sure the type constructor of the class is in the appropriate

112+ -- uniqueness hierarchy

113+ chkUniq u@(PUniverse _) PType = u

114+ chkUniq (PUniverse l) (PUniverse r) = PUniverse (min l r)

115+ chkUniq (PPi _ _ _ sc) t = chkUniq sc t

116+ chkUniq _ t = t

110117

111118 mdec :: Name -> Name

112119 mdec (UN n) = SN (MethodN (UN n))

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

@@ -271,7 +271,8 @@ elabCon info syn tn codata expkind dkind (doc, argDocs, n, t_in, fc, forcenames)

271271 getNamePos _ _ _ = Nothing

272272

273273 -- if the constructor is a UniqueType, the datatype must be too

274− -- (Type* is fine, since that is checked for uniqueness too)

274+ -- (AnyType is fine, since that is checked for uniqueness too)

275+ -- if hte contructor is AnyType, the datatype must be at least AnyType

275276 checkUniqueKind (UType NullType) (UType NullType) = return ()

276277 checkUniqueKind (UType NullType) _

277278 = tclift $ tfail (At fc (UniqueKindError NullType n))

@@ -279,7 +280,10 @@ elabCon info syn tn codata expkind dkind (doc, argDocs, n, t_in, fc, forcenames)

279280 checkUniqueKind (UType UniqueType) (UType AllTypes) = return ()

280281 checkUniqueKind (UType UniqueType) _

281282 = tclift $ tfail (At fc (UniqueKindError UniqueType n))

282− checkUniqueKind (UType AllTypes) _ = return ()

283+ checkUniqueKind (UType AllTypes) (UType AllTypes) = return ()

284+ checkUniqueKind (UType AllTypes) (UType UniqueType) = return ()

285+ checkUniqueKind (UType AllTypes) _

286+ = tclift $ tfail (At fc (UniqueKindError AllTypes n))

283287 checkUniqueKind _ _ = return ()

284288

285289 -- Constructor's kind must be <= expected kind

src/Idris/ParseExpr.hs+1

@@ -330,6 +330,7 @@ simpleExpr syn =

330330 <|> proofExpr syn

331331 <|> tacticsExpr syn

332332 <|> try (do reserved "Type"; symbol "*"; return $ PUniverse AllTypes)

333+ <|> do reserved "AnyType"; return $ PUniverse AllTypes

333334 <|> do reserved "Type"; return PType

334335 <|> do reserved "UniqueType"; return $ PUniverse UniqueType

335336 <|> do reserved "NullType"; return $ PUniverse NullType

test/unique001/unique001c.idr+3−3

@@ -25,7 +25,7 @@ share : UTree -> Tree

2525share ULeaf = Leaf

2626share (UNode x y z) = Node (share x) y (share z)

2727

28−class UFunctor (f : Type -> Type*) where

28+class UFunctor (f : Type -> AnyType) where

2929 fmap : (a -> b) -> f a -> f b

3030

3131instance UFunctor List where

@@ -36,10 +36,10 @@ instance UFunctor UList where

3636 fmap f UNil = UNil

3737 fmap f (UCons x xs) = UCons (f x) (fmap f xs)

3838

39−uconst : {a : Type*} -> a -> b -> a

39+uconst : {a : AnyType} -> a -> b -> a

4040uconst x y = x

4141

42−data MPair : Type* -> Type* -> Type* where

42+data MPair : AnyType -> AnyType -> AnyType where

4343 MkMPair : {a, b : Type*} -> a -> b -> MPair a b

4444

4545ndup : {a : UniqueType} -> a -> UPair a a