d1941f5 · Idris-dev · git.iko.soy

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

compare with master

unifiedsplit

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

653instance Show Universe where

654 show UniqueType = "UniqueType"

655 show NullType = "NullType"

656− show AllTypes = "Type*"

656+ show AllTypes = "AnyType"

657

658data Raw = Var Name

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

106 where

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

108 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

110

117

111 mdec :: Name -> Name

118 mdec :: Name -> Name

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

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

271 getNamePos _ _ _ = Nothing

272

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

275 checkUniqueKind (UType NullType) (UType NullType) = return ()

276 checkUniqueKind (UType NullType) (UType NullType) = return ()

276 checkUniqueKind (UType NullType) _

277 checkUniqueKind (UType NullType) _

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

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

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

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

280 checkUniqueKind (UType UniqueType) _

281 checkUniqueKind (UType UniqueType) _

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

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

283 checkUniqueKind _ _ = return ()

287 checkUniqueKind _ _ = return ()

284

288

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

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

src/Idris/ParseExpr.hs+1

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

330 <|> proofExpr syn

331 <|> tacticsExpr syn

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

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

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

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

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

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

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

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

test/unique001/unique001c.idr+3−3

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

25share ULeaf = Leaf

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

27

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

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

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

30

31instance UFunctor List where

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

36 fmap f UNil = UNil

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

38

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

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

40uconst x y = x

41

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

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

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

44

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