git.iko.soy/Idris-dev
on master help sign in
Check constructor kinds for uniqueness errors
41e9032Edwin Brady
src/Idris/Core/TT.hs+1
compare with master
unifiedsplit
@@ -138,6 +138,7 @@ data Err' t
138 | IncompleteTerm t
138 | IncompleteTerm t
139 | UniverseError
139 | UniverseError
140 | UniqueError Name
140 | UniqueError Name
141+ | UniqueKindError Name
141 | ProgramLineComment
142 | ProgramLineComment
142 | Inaccessible Name
143 | Inaccessible Name
143 | NonCollapsiblePostulate Name
144 | NonCollapsiblePostulate Name
src/Idris/Delaborate.hs+2
@@ -226,6 +226,8 @@ pprintErr' i (IncompleteTerm t) = text "Incomplete term" <+> annTm t (pprintTerm
226pprintErr' i UniverseError = text "Universe inconsistency"
226pprintErr' i UniverseError = text "Universe inconsistency"
227pprintErr' i (UniqueError n) = text "Unique name" <+> annName' n (showbasic n)
227pprintErr' i (UniqueError n) = text "Unique name" <+> annName' n (showbasic n)
228 <+> text "is used more than once"
228 <+> 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"
229pprintErr' i ProgramLineComment = text "Program line next to comment"
231pprintErr' i ProgramLineComment = text "Program line next to comment"
230pprintErr' i (Inaccessible n) = annName n <+> text "is not an accessible pattern variable"
232pprintErr' i (Inaccessible n) = annName n <+> text "is not an accessible pattern variable"
231pprintErr' i (NonCollapsiblePostulate n) = text "The return type of postulate" <+>
233pprintErr' 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)
54 = do let codata = Codata `elem` opts
54 = do let codata = Codata `elem` opts
55 iLOG (show (fc, doc))
55 iLOG (show (fc, doc))
56 checkUndefined fc n
56 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
58
58
59 addIBC (IBCDef n)
59 addIBC (IBCDef n)
60 updateContext (addTyDecl n (TCon 0 0) cty) -- temporary, to check cons
60 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)
63 = do let codata = Codata `elem` opts
63 = do let codata = Codata `elem` opts
64 iLOG (show fc)
64 iLOG (show fc)
65 undef <- isUndefined fc n
65 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
67 -- if n is defined already, make sure it is just a type declaration
67 -- if n is defined already, make sure it is just a type declaration
68 -- with the same type we've just elaborated
68 -- with the same type we've just elaborated
69 i <- getIState
69 i <- getIState
@@ -71,7 +71,7 @@ elabData info syn doc argDocs fc opts (PDatadecl n t_in dcons)
71 -- temporary, to check cons
71 -- temporary, to check cons
72 when undef $ updateContext (addTyDecl n (TCon 0 0) cty)
72 when undef $ updateContext (addTyDecl n (TCon 0 0) cty)
73 let cnameinfo = cinfo info (map cname dcons)
73 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
75 ttag <- getName
75 ttag <- getName
76 i <- getIState
76 i <- getIState
77 let as = map (const Nothing) (getArgTys cty)
77 let as = map (const Nothing) (getArgTys cty)
@@ -203,12 +203,15 @@ elabData info syn doc argDocs fc opts (PDatadecl n t_in dcons)
203-- TODO: the above is a comment from the past;
203-- TODO: the above is a comment from the past;
204-- forcenames is probably no longer needed
204-- forcenames is probably no longer needed
205elabCon :: ElabInfo -> SyntaxInfo -> Name -> Bool ->
205elabCon :: ElabInfo -> SyntaxInfo -> Name -> Bool ->
206+ Type -> -- for kind checking
206− (Docstring, [(Name, Docstring)], Name, PTerm, FC, [Name]) -> Idris (Name, Type)
207+ (Docstring, [(Name, Docstring)], Name, PTerm, FC, [Name]) ->
208+ Idris (Name, Type)
207−elabCon info syn tn codata (doc, argDocs, n, t_in, fc, forcenames)
209+elabCon info syn tn codata expkind (doc, argDocs, n, t_in, fc, forcenames)
208 = do checkUndefined fc n
210 = 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)
210 ctxt <- getContext
212 ctxt <- getContext
211 let cty' = normalise ctxt [] cty
213 let cty' = normalise ctxt [] cty
214+ checkUniqueKind ckind expkind
212
215
213 -- Check that the constructor type is, in fact, a part of the family being defined
216 -- Check that the constructor type is, in fact, a part of the family being defined
214 tyIs n cty'
217 tyIs n cty'
@@ -250,6 +253,15 @@ elabCon info syn tn codata (doc, argDocs, n, t_in, fc, forcenames)
250 | otherwise = getNamePos (i + 1) sc x
253 | otherwise = getNamePos (i + 1) sc x
251 getNamePos _ _ _ = Nothing
254 getNamePos _ _ _ = Nothing
252
255
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+
253type EliminatorState = StateT (Map.Map String Int) Idris
265type EliminatorState = StateT (Map.Map String Int) Idris
254
266
255-- TODO: Rewrite everything to use idris_implicits instead of manual splitting (or in TT)
267-- 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)
49import Util.Pretty(pretty, text)
49import Util.Pretty(pretty, text)
50
50
51buildType :: ElabInfo -> SyntaxInfo -> FC -> FnOpts -> Name -> PTerm ->
51buildType :: ElabInfo -> SyntaxInfo -> FC -> FnOpts -> Name -> PTerm ->
52− Idris (Type, PTerm, [(Int, Name)])
52+ Idris (Type, Type, PTerm, [(Int, Name)])
53buildType info syn fc opts n ty' = do
53buildType info syn fc opts n ty' = do
54 ctxt <- getContext
54 ctxt <- getContext
55 i <- getIState
55 i <- getIState
@@ -80,7 +80,7 @@ buildType info syn fc opts n ty' = do
80 logLvl 5 $ "Rechecking"
80 logLvl 5 $ "Rechecking"
81 logLvl 6 $ show tyT
81 logLvl 6 $ show tyT
82 logLvl 10 $ "Elaborated to " ++ showEnvDbg [] tyT
82 logLvl 10 $ "Elaborated to " ++ showEnvDbg [] tyT
83− (cty, _) <- recheckC fc [] tyT
83+ (cty, ckind) <- recheckC fc [] tyT
84
84
85 -- record the implicit and inaccessible arguments
85 -- record the implicit and inaccessible arguments
86 i <- getIState
86 i <- getIState
@@ -99,7 +99,7 @@ buildType info syn fc opts n ty' = do
99 setFnInfo n fninfo
99 setFnInfo n fninfo
100 addIBC (IBCFnInfo n fninfo)
100 addIBC (IBCFnInfo n fninfo)
101
101
102− return (cty, ty, inacc)
102+ return (cty, ckind, ty, inacc)
103 where
103 where
104 patToImp (Bind n (PVar t) sc) = Bind n (Pi t) (patToImp sc)
104 patToImp (Bind n (PVar t) sc) = Bind n (Pi t) (patToImp sc)
105 patToImp (Bind n b sc) = Bind n b (patToImp sc)
105 patToImp (Bind n b sc) = Bind n b (patToImp sc)
@@ -121,7 +121,7 @@ elabType' :: Bool -> -- normalise it
121elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params info) ty_in
121elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params info) ty_in
122 n = liftname info n_in in -}
122 n = liftname info n_in in -}
123 do checkUndefined fc n
123 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'
125
125
126 addStatics n cty ty
126 addStatics n cty ty
127 let nty = cty -- normalise ctxt [] cty
127 let nty = cty -- normalise ctxt [] cty