git.iko.soy/Idris-dev
on master help sign in
Check constructor kinds for uniqueness errors
commit41e90320c631db5260b0404d871f73b2c676409b authorEdwin Brady <ecb10@st-andrews.ac.uk> dateThu 14 Aug 2014, 10:25 (12 years ago) parent7cc7c32
4 files changed+25−10
compare with master
unifiedsplit
src/Idris/Core/TT.hs+1 src/Idris/Delaborate.hs+2 src/Idris/Elab/Data.hs+18−6 src/Idris/Elab/Type.hs+4−4
src/Idris/Core/TT.hs+1
@@ -138,6 +138,7 @@ data Err' t
138138 | IncompleteTerm t
139139 | UniverseError
140140 | UniqueError Name
141+ | UniqueKindError Name
141142 | ProgramLineComment
142143 | Inaccessible Name
143144 | NonCollapsiblePostulate Name
src/Idris/Delaborate.hs+2
@@ -226,6 +226,8 @@ pprintErr' i (IncompleteTerm t) = text "Incomplete term" <+> annTm t (pprintTerm
226226pprintErr' i UniverseError = text "Universe inconsistency"
227227pprintErr' i (UniqueError n) = text "Unique name" <+> annName' n (showbasic n)
228228 <+> text "is used more than once"
229+pprintErr' i (UniqueKindError n) = text "Constructor" <+> annName' n (showbasic n)
230+ <+> text "has a UniqueType, but the data type deos not"
229231pprintErr' i ProgramLineComment = text "Program line next to comment"
230232pprintErr' i (Inaccessible n) = annName n <+> text "is not an accessible pattern variable"
231233pprintErr' i (NonCollapsiblePostulate n) = text "The return type of postulate" <+>
src/Idris/Elab/Data.hs+18−6
@@ -54,7 +54,7 @@ elabData info syn doc argDocs fc opts (PLaterdecl n t_in)
5454 = do let codata = Codata `elem` opts
5555 iLOG (show (fc, doc))
5656 checkUndefined fc n
57− (cty, t, inacc) <- buildType info syn fc [] n t_in
57+ (cty, _, t, inacc) <- buildType info syn fc [] n t_in
5858
5959 addIBC (IBCDef n)
6060 updateContext (addTyDecl n (TCon 0 0) cty) -- temporary, to check cons
@@ -63,7 +63,7 @@ elabData info syn doc argDocs fc opts (PDatadecl n t_in dcons)
6363 = do let codata = Codata `elem` opts
6464 iLOG (show fc)
6565 undef <- isUndefined fc n
66− (cty, t, inacc) <- buildType info syn fc [] n t_in
66+ (cty, _, t, inacc) <- buildType info syn fc [] n t_in
6767 -- if n is defined already, make sure it is just a type declaration
6868 -- with the same type we've just elaborated
6969 i <- getIState
@@ -71,7 +71,7 @@ elabData info syn doc argDocs fc opts (PDatadecl n t_in dcons)
7171 -- temporary, to check cons
7272 when undef $ updateContext (addTyDecl n (TCon 0 0) cty)
7373 let cnameinfo = cinfo info (map cname dcons)
74− cons <- mapM (elabCon cnameinfo syn n codata) dcons
74+ cons <- mapM (elabCon cnameinfo syn n codata (getRetTy cty)) dcons
7575 ttag <- getName
7676 i <- getIState
7777 let as = map (const Nothing) (getArgTys cty)
@@ -203,12 +203,15 @@ elabData info syn doc argDocs fc opts (PDatadecl n t_in dcons)
203203-- TODO: the above is a comment from the past;
204204-- forcenames is probably no longer needed
205205elabCon :: ElabInfo -> SyntaxInfo -> Name -> Bool ->
206− (Docstring, [(Name, Docstring)], Name, PTerm, FC, [Name]) -> Idris (Name, Type)
207−elabCon info syn tn codata (doc, argDocs, n, t_in, fc, forcenames)
206+ Type -> -- for kind checking
207+ (Docstring, [(Name, Docstring)], Name, PTerm, FC, [Name]) ->
208+ Idris (Name, Type)
209+elabCon info syn tn codata expkind (doc, argDocs, n, t_in, fc, forcenames)
208210 = do checkUndefined fc n
209− (cty, t, inacc) <- buildType info syn fc [Constructor] n (if codata then mkLazy t_in else t_in)
211+ (cty, ckind, t, inacc) <- buildType info syn fc [Constructor] n (if codata then mkLazy t_in else t_in)
210212 ctxt <- getContext
211213 let cty' = normalise ctxt [] cty
214+ checkUniqueKind ckind expkind
212215
213216 -- Check that the constructor type is, in fact, a part of the family being defined
214217 tyIs n cty'
@@ -250,6 +253,15 @@ elabCon info syn tn codata (doc, argDocs, n, t_in, fc, forcenames)
250253 | otherwise = getNamePos (i + 1) sc x
251254 getNamePos _ _ _ = Nothing
252255
256+ -- if the constructor is a UniqueType, the datatype must be too
257+ -- (Type* is fine, since that is checked for uniqueness too)
258+ checkUniqueKind (UType UniqueType) (UType UniqueType) = return ()
259+ checkUniqueKind (UType UniqueType) (UType AllTypes) = return ()
260+ checkUniqueKind (UType UniqueType) (TType _)
261+ = tclift $ tfail (UniqueKindError n)
262+ checkUniqueKind (UType AllTypes) _ = return ()
263+ checkUniqueKind (TType _) _ = return ()
264+
253265type EliminatorState = StateT (Map.Map String Int) Idris
254266
255267-- TODO: Rewrite everything to use idris_implicits instead of manual splitting (or in TT)
src/Idris/Elab/Type.hs+4−4
@@ -49,7 +49,7 @@ import Data.List.Split (splitOn)
4949import Util.Pretty(pretty, text)
5050
5151buildType :: ElabInfo -> SyntaxInfo -> FC -> FnOpts -> Name -> PTerm ->
52− Idris (Type, PTerm, [(Int, Name)])
52+ Idris (Type, Type, PTerm, [(Int, Name)])
5353buildType info syn fc opts n ty' = do
5454 ctxt <- getContext
5555 i <- getIState
@@ -80,7 +80,7 @@ buildType info syn fc opts n ty' = do
8080 logLvl 5 $ "Rechecking"
8181 logLvl 6 $ show tyT
8282 logLvl 10 $ "Elaborated to " ++ showEnvDbg [] tyT
83− (cty, _) <- recheckC fc [] tyT
83+ (cty, ckind) <- recheckC fc [] tyT
8484
8585 -- record the implicit and inaccessible arguments
8686 i <- getIState
@@ -99,7 +99,7 @@ buildType info syn fc opts n ty' = do
9999 setFnInfo n fninfo
100100 addIBC (IBCFnInfo n fninfo)
101101
102− return (cty, ty, inacc)
102+ return (cty, ckind, ty, inacc)
103103 where
104104 patToImp (Bind n (PVar t) sc) = Bind n (Pi t) (patToImp sc)
105105 patToImp (Bind n b sc) = Bind n b (patToImp sc)
@@ -121,7 +121,7 @@ elabType' :: Bool -> -- normalise it
121121elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params info) ty_in
122122 n = liftname info n_in in -}
123123 do checkUndefined fc n
124− (cty, ty, inacc) <- buildType info syn fc opts n ty'
124+ (cty, _, ty, inacc) <- buildType info syn fc opts n ty'
125125
126126 addStatics n cty ty
127127 let nty = cty -- normalise ctxt [] cty