git.iko.soy/Idris-dev
on master help sign in
Merge branch 'improve-universe-solver' of https://github.com/ozgurakgun/Idris-dev into ozgurakgun-improve-universe-solver
cc9895dEdwin Brady
src/Idris/Core/Constraints.hs+72−22
compare with master
unifiedsplit
@@ -62,14 +62,34 @@ solve maxUniverseLevel ucs =
62 ]
62 ]
63 }
63 }
64
64
65+ lhs (ULT (UVar x) _) = Just (Var x)
66+ lhs (ULE (UVar x) _) = Just (Var x)
67+ lhs _ = Nothing
68+
69+ rhs (ULT _ (UVar x)) = Just (Var x)
70+ rhs (ULE _ (UVar x)) = Just (Var x)
71+ rhs _ = Nothing
72+
65− -- | a map from variables to the list of constraints the variable occurs in.
73+ -- | a map from variables to the list of constraints the variable occurs in. (in the LHS of a constraint)
66− constraints :: M.Map Var (S.Set ConstraintFC)
74+ constraintsLHS :: M.Map Var (S.Set (UConstraint, FC))
67− constraints = M.fromListWith S.union
75+ constraintsLHS = M.fromListWith S.union
68− [ (v, S.singleton (ConstraintFC c fc))
76+ [ (v, S.singleton (c,fc))
69− | ConstraintFC c fc <- inpConstraints
77+ | (c, fc) <- inpConstraints
70 , let vars = varsIn c
78 , let vars = varsIn c
71 , length vars > 1 -- do not register unary constraints
79 , length vars > 1 -- do not register unary constraints
72 , v <- vars
80 , v <- vars
81+ , lhs c == Just v
82+ ]
83+
84+ -- | a map from variables to the list of constraints the variable occurs in. (in the RHS of a constraint)
85+ constraintsRHS :: M.Map Var (S.Set (UConstraint, FC))
86+ constraintsRHS = M.fromListWith S.union
87+ [ (v, S.singleton (c,fc))
88+ | (c, fc) <- inpConstraints
89+ , let vars = varsIn c
90+ , length vars > 1 -- do not register unary constraints
91+ , v <- vars
92+ , rhs c == Just v
73 ]
93 ]
74
94
75 -- | this is where the actual work is done.
95 -- | this is where the actual work is done.
@@ -87,15 +107,15 @@ solve maxUniverseLevel ucs =
87 ULE a b -> do
107 ULE a b -> do
88 Domain lowerA upperA <- domainOf a
108 Domain lowerA upperA <- domainOf a
89 Domain lowerB upperB <- domainOf b
109 Domain lowerB upperB <- domainOf b
90− when (upperB < upperA) $ updateDomainOf (ConstraintFC cons fc) a (Domain lowerA upperB)
110+ when (upperB < upperA) $ updateUpperBoundOf (cons, fc) a upperB
91− when (lowerA > lowerB) $ updateDomainOf (ConstraintFC cons fc) b (Domain lowerA upperB)
111+ when (lowerA > lowerB) $ updateLowerBoundOf (cons, fc) b lowerA
92 ULT a b -> do
112 ULT a b -> do
93 Domain lowerA upperA <- domainOf a
113 Domain lowerA upperA <- domainOf a
94 Domain lowerB upperB <- domainOf b
114 Domain lowerB upperB <- domainOf b
95 let upperB_pred = pred upperB
115 let upperB_pred = pred upperB
96 let lowerA_succ = succ lowerA
116 let lowerA_succ = succ lowerA
97− when (upperB_pred < upperA) $ updateDomainOf (ConstraintFC cons fc) a (Domain lowerA upperB_pred)
117+ when (upperB_pred < upperA) $ updateUpperBoundOf (cons, fc) a upperB_pred
98− when (lowerA_succ > lowerB) $ updateDomainOf (ConstraintFC cons fc) b (Domain lowerA_succ upperB)
118+ when (lowerA_succ > lowerB) $ updateLowerBoundOf (cons, fc) b lowerA_succ
99 propagate
119 propagate
100
120
101 -- | extract a solution from the state.
121 -- | extract a solution from the state.
@@ -121,13 +141,12 @@ solve maxUniverseLevel ucs =
121 domainOf (UVar var) = gets (fst . (M.! Var var) . domainStore)
141 domainOf (UVar var) = gets (fst . (M.! Var var) . domainStore)
122 domainOf (UVal val) = return (Domain val val)
142 domainOf (UVal val) = return (Domain val val)
123
143
124− -- | updates the domain of a variable.
125− -- this function is also where we fail, inc ase of a domain wipe-out.
126− updateDomainOf :: ConstraintFC -> UExp -> Domain -> StateT SolverState TC ()
144+ updateUpperBoundOf :: (UConstraint, FC) -> UExp -> Int -> StateT SolverState TC ()
127− updateDomainOf suspect (UVar var) newDom = do
145+ updateUpperBoundOf suspect (UVar var) upper = do
128 doms <- gets domainStore
146 doms <- gets domainStore
129− let (oldDom, suspects) = doms M.! Var var
147+ let (oldDom@(Domain lower _), suspects) = doms M.! Var var
148+ let newDom = Domain lower upper
130− when (wipeOut newDom) $ lift $ Error $ At (ufc suspect) $ Msg $ unlines
149+ when (wipeOut newDom) $ lift $ Error $ At (snd suspect) $ Msg $ unlines
131 $ "Universe inconsistency."
150 $ "Universe inconsistency."
132 : ("Working on: " ++ show (UVar var))
151 : ("Working on: " ++ show (UVar var))
133 : ("Old domain: " ++ show oldDom)
152 : ("Old domain: " ++ show oldDom)
@@ -135,17 +154,48 @@ solve maxUniverseLevel ucs =
135 : "Involved constraints: "
154 : "Involved constraints: "
136 : map (("\t"++) . show) (suspect : S.toList suspects)
155 : map (("\t"++) . show) (suspect : S.toList suspects)
137 modify $ \ st -> st { domainStore = M.insert (Var var) (newDom, S.insert suspect suspects) doms }
156 modify $ \ st -> st { domainStore = M.insert (Var var) (newDom, S.insert suspect suspects) doms }
138− addToQueue (Var var)
157+ addToQueueRHS (fst suspect) (Var var)
139− updateDomainOf _ UVal{} _ = return ()
158+ updateUpperBoundOf _ UVal{} _ = return ()
159+
160+ updateLowerBoundOf :: (UConstraint, FC) -> UExp -> Int -> StateT SolverState TC ()
161+ updateLowerBoundOf suspect (UVar var) lower = do
162+ doms <- gets domainStore
163+ let (oldDom@(Domain _ upper), suspects) = doms M.! Var var
164+ let newDom = Domain lower upper
165+ when (wipeOut newDom) $ lift $ Error $ At (snd suspect) $ Msg $ unlines
166+ $ "Universe inconsistency."
167+ : ("Working on: " ++ show (UVar var))
168+ : ("Old domain: " ++ show oldDom)
169+ : ("New domain: " ++ show newDom)
170+ : "Involved constraints: "
171+ : map (("\t"++) . show) (suspect : S.toList suspects)
172+ modify $ \ st -> st { domainStore = M.insert (Var var) (newDom, S.insert suspect suspects) doms }
173+ addToQueueLHS (fst suspect) (Var var)
174+ updateLowerBoundOf _ UVal{} _ = return ()
175+
176+ -- | add all constraints (with the given var on the lhs) to the queue
177+ addToQueueLHS :: MonadState SolverState m => UConstraint -> Var -> m ()
178+ addToQueueLHS thisCons var =
179+ case M.lookup var constraintsLHS of
180+ Nothing -> return ()
181+ Just cs -> do
182+ Queue list set <- gets queue
183+ let set' = S.insert thisCons set
184+ let newCons = [ c | c <- S.toList cs, fst c `S.notMember` set' ]
185+ if null newCons
186+ then return ()
187+ else modify $ \ st -> st { queue = Queue (list ++ newCons)
188+ (S.union set (S.fromList (map fst newCons))) }
140
189
141− -- | add all constraints related to a variable.
190+ -- | add all constraints (with the given var on the rhs) to the queue
142− addToQueue :: MonadState SolverState m => Var -> m ()
191+ addToQueueRHS :: MonadState SolverState m => UConstraint -> Var -> m ()
143− addToQueue var =
192+ addToQueueRHS thisCons var =
144− case M.lookup var constraints of
193+ case M.lookup var constraintsRHS of
145 Nothing -> return ()
194 Nothing -> return ()
146 Just cs -> do
195 Just cs -> do
147 Queue list set <- gets queue
196 Queue list set <- gets queue
197+ let set' = S.insert thisCons set
148− let newCons = [ c | c <- S.toList cs, uconstraint c `S.notMember` set ]
198+ let newCons = [ c | c <- S.toList cs, fst c `S.notMember` set' ]
149 if null newCons
199 if null newCons
150 then return ()
200 then return ()
151 else modify $ \ st -> st { queue = Queue (list ++ newCons)
201 else modify $ \ st -> st { queue = Queue (list ++ newCons)
src/Idris/Core/Typecheck.hs+62−30
@@ -69,7 +69,7 @@ check ctxt env tm
69 = evalStateT (check' True ctxt env tm) (0, []) -- Holes allowed
69 = evalStateT (check' True ctxt env tm) (0, []) -- Holes allowed
70
70
71check' :: Bool -> Context -> Env -> Raw -> StateT UCs TC (Term, Type)
71check' :: Bool -> Context -> Env -> Raw -> StateT UCs TC (Term, Type)
72−check' holes ctxt env top = chk (TType (UVar (-5))) env top where
72+check' holes ctxt env top = chk (TType (UVar (-5))) Nothing env top where
73
73
74 smaller (UType NullType) _ = UType NullType
74 smaller (UType NullType) _ = UType NullType
75 smaller _ (UType NullType) = UType NullType
75 smaller _ (UType NullType) = UType NullType
@@ -78,23 +78,47 @@ check' holes ctxt env top = chk (TType (UVar (-5))) env top where
78 smaller x _ = x
78 smaller x _ = x
79
79
80 chk :: Type -> -- uniqueness level
80 chk :: Type -> -- uniqueness level
81+ Maybe UExp -> -- maximum universe level, if known
81 Env -> Raw -> StateT UCs TC (Term, Type)
82 Env -> Raw -> StateT UCs TC (Term, Type)
82− chk u env (Var n)
83+ chk u maxu env (Var n)
83 | Just (i, ty) <- lookupTyEnv n env = return (P Bound n ty, ty)
84 | Just (i, ty) <- lookupTyEnv n env = return (P Bound n ty, ty)
84 -- If we're elaborating, we don't want the private names; if we're
85 -- If we're elaborating, we don't want the private names; if we're
85 -- checking an already elaborated term, we do
86 -- checking an already elaborated term, we do
86 | (P nt n' ty : _) <- lookupP_all (not holes) n ctxt
87 | (P nt n' ty : _) <- lookupP_all (not holes) n ctxt
87 = return (P nt n' ty, ty)
88 = return (P nt n' ty, ty)
88 | otherwise = do lift $ tfail $ NoSuchVariable n
89 | otherwise = do lift $ tfail $ NoSuchVariable n
89− chk u env ap@(RApp f a)
90+ chk u maxu env ap@(RApp f RType) | not holes
91+ -- special case to reduce constraintss
90− = do (fv, fty) <- chk u env f
92+ = do (fv, fty) <- chk u maxu env f
91− (av, aty) <- chk u env a
92 let fty' = case uniqueBinders (map fst env) (finalise fty) of
93 let fty' = case uniqueBinders (map fst env) (finalise fty) of
93 ty@(Bind x (Pi i s k) t) -> ty
94 ty@(Bind x (Pi i s k) t) -> ty
94 _ -> uniqueBinders (map fst env)
95 _ -> uniqueBinders (map fst env)
95 $ case hnf ctxt env fty of
96 $ case hnf ctxt env fty of
96 ty@(Bind x (Pi i s k) t) -> ty
97 ty@(Bind x (Pi i s k) t) -> ty
97 _ -> normalise ctxt env fty
98 _ -> normalise ctxt env fty
99+ case fty' of
100+ Bind x (Pi i (TType v') k) t ->
101+ do (v, cs) <- get
102+ put (v+1, ULT (UVar v) v' : cs)
103+ let apty = simplify initContext env
104+ (Bind x (Let (TType v') (TType (UVar v))) t)
105+ return (App fv (TType (UVar v)), apty)
106+ Bind x (Pi i s k) t ->
107+ do (av, aty) <- chk u maxu env RType
108+ convertsC ctxt env aty s
109+ let apty = simplify initContext env
110+ (Bind x (Let aty av) t)
111+ return (App fv av, apty)
112+ t -> lift $ tfail $ NonFunctionType fv fty
113+ chk u maxu env ap@(RApp f a)
114+ = do (fv, fty) <- chk u maxu env f
115+ let fty' = case uniqueBinders (map fst env) (finalise fty) of
116+ ty@(Bind x (Pi i s k) t) -> ty
117+ _ -> uniqueBinders (map fst env)
118+ $ case hnf ctxt env fty of
119+ ty@(Bind x (Pi i s k) t) -> ty
120+ _ -> normalise ctxt env fty
121+ (av, aty) <- chk u maxu env a
98 case fty' of
122 case fty' of
99 Bind x (Pi i s k) t ->
123 Bind x (Pi i s k) t ->
100 do convertsC ctxt env aty s
124 do convertsC ctxt env aty s
@@ -102,13 +126,13 @@ check' holes ctxt env top = chk (TType (UVar (-5))) env top where
102 (Bind x (Let aty av) t)
126 (Bind x (Let aty av) t)
103 return (App fv av, apty)
127 return (App fv av, apty)
104 t -> lift $ tfail $ NonFunctionType fv fty
128 t -> lift $ tfail $ NonFunctionType fv fty
105− chk u env RType
129+ chk u maxu env RType
106 | holes = return (TType (UVal 0), TType (UVal 0))
130 | holes = return (TType (UVal 0), TType (UVal 0))
107 | otherwise = do (v, cs) <- get
131 | otherwise = do (v, cs) <- get
108 let c = ULT (UVar v) (UVar (v+1))
132 let c = ULT (UVar v) (UVar (v+1))
109 put (v+2, (c:cs))
133 put (v+2, (c:cs))
110 return (TType (UVar v), TType (UVar (v+1)))
134 return (TType (UVar v), TType (UVar (v+1)))
111− chk u env (RUType un)
135+ chk u maxu env (RUType un)
112 | holes = return (UType un, TType (UVal 0))
136 | holes = return (UType un, TType (UVal 0))
113 | otherwise = do -- TODO! Issue #1715 on the issue tracker.
137 | otherwise = do -- TODO! Issue #1715 on the issue tracker.
114 -- https://github.com/idris-lang/Idris-dev/issues/1715
138 -- https://github.com/idris-lang/Idris-dev/issues/1715
@@ -117,8 +141,8 @@ check' holes ctxt env top = chk (TType (UVar (-5))) env top where
117 -- put (v+2, (c:cs))
141 -- put (v+2, (c:cs))
118 -- return (TType (UVar v), TType (UVar (v+1)))
142 -- return (TType (UVar v), TType (UVar (v+1)))
119 return (UType un, TType (UVal 0))
143 return (UType un, TType (UVal 0))
120− chk u env (RConstant Forgot) = return (Erased, Erased)
144+ chk u maxu env (RConstant Forgot) = return (Erased, Erased)
121− chk u env (RConstant c) = return (Constant c, constType c)
145+ chk u maxu env (RConstant c) = return (Constant c, constType c)
122 where constType (I _) = Constant (AType (ATInt ITNative))
146 where constType (I _) = Constant (AType (ATInt ITNative))
123 constType (BI _) = Constant (AType (ATInt ITBig))
147 constType (BI _) = Constant (AType (ATInt ITBig))
124 constType (Fl _) = Constant (AType ATFloat)
148 constType (Fl _) = Constant (AType ATFloat)
@@ -135,17 +159,25 @@ check' holes ctxt env top = chk (TType (UVar (-5))) env top where
135 constType TheWorld = Constant WorldType
159 constType TheWorld = Constant WorldType
136 constType Forgot = Erased
160 constType Forgot = Erased
137 constType _ = TType (UVal 0)
161 constType _ = TType (UVal 0)
138− chk u env (RForce t) = do (_, ty) <- chk u env t
162+ chk u maxu env (RForce t) = do (_, ty) <- chk u maxu env t
139− return (Erased, ty)
163+ return (Erased, ty)
140− chk u env (RBind n (Pi i s k) t)
164+ chk u maxu env (RBind n (Pi i s k) t)
141− = do (sv, st) <- chk u env s
165+ = do (sv, st) <- chk u Nothing env s
166+ vcs <- get
142− (kv, kt) <- chk u env k
167+ (kv, kt) <- chk u Nothing env k
143− (tv, tt) <- chk st ((n, Pi i sv kv) : env) t
168+ put vcs -- no need to validate these constraints, they are independent
144 (v, cs) <- get
169 (v, cs) <- get
170+ nmaxu <- case maxu of
171+ Nothing -> do put (v+1, cs)
172+ return (UVar v)
173+ Just m -> return m
174+ (tv, tt) <- chk st (Just nmaxu) ((n, Pi i sv kv) : env) t
145 case (normalise ctxt env st, normalise ctxt env tt) of
175 case (normalise ctxt env st, normalise ctxt env tt) of
146 (TType su, TType tu) -> do
176 (TType su, TType tu) -> do
147− when (not holes) $ put (v+1, ULE su (UVar v):ULE tu (UVar v):cs)
177+ when (not holes) $ do (v, cs) <- get
178+ put (v, ULE su nmaxu :
179+ ULE tu nmaxu : cs)
148− let k' = st `smaller` kv `smaller` TType (UVar v) `smaller` u
180+ let k' = TType (UVar v) `smaller` st `smaller` kv `smaller` u
149 return (Bind n (Pi i (uniqueBinders (map fst env) sv) k')
181 return (Bind n (Pi i (uniqueBinders (map fst env) sv) k')
150 (pToV n tv), k')
182 (pToV n tv), k')
151 (un, un') ->
183 (un, un') ->
@@ -168,27 +200,27 @@ check' holes ctxt env top = chk (TType (UVar (-5))) env top where
168 mostUnique (Pi _ _ pk : es) k = mostUnique es (smaller pk k)
200 mostUnique (Pi _ _ pk : es) k = mostUnique es (smaller pk k)
169 mostUnique (_ : es) k = mostUnique es k
201 mostUnique (_ : es) k = mostUnique es k
170
202
171− chk u env (RBind n b sc)
203+ chk u maxu env (RBind n b sc)
172 = do (b', bt') <- checkBinder b
204 = do (b', bt') <- checkBinder b
173− (scv, sct) <- chk (smaller bt' u) ((n, b'):env) sc
205+ (scv, sct) <- chk (smaller bt' u) maxu ((n, b'):env) sc
174 discharge n b' bt' (pToV n scv) (pToV n sct)
206 discharge n b' bt' (pToV n scv) (pToV n sct)
175 where checkBinder (Lam t)
207 where checkBinder (Lam t)
176− = do (tv, tt) <- chk u env t
208+ = do (tv, tt) <- chk u maxu env t
177 let tv' = normalise ctxt env tv
209 let tv' = normalise ctxt env tv
178 let tt' = normalise ctxt env tt
210 let tt' = normalise ctxt env tt
179 lift $ isType ctxt env tt'
211 lift $ isType ctxt env tt'
180 return (Lam tv, tt')
212 return (Lam tv, tt')
181 checkBinder (Let t v)
213 checkBinder (Let t v)
182− = do (tv, tt) <- chk u env t
214+ = do (tv, tt) <- chk u maxu env t
183− (vv, vt) <- chk u env v
215+ (vv, vt) <- chk u maxu env v
184 let tv' = normalise ctxt env tv
216 let tv' = normalise ctxt env tv
185 let tt' = normalise ctxt env tt
217 let tt' = normalise ctxt env tt
186 convertsC ctxt env vt tv
218 convertsC ctxt env vt tv
187 lift $ isType ctxt env tt'
219 lift $ isType ctxt env tt'
188 return (Let tv vv, tt')
220 return (Let tv vv, tt')
189 checkBinder (NLet t v)
221 checkBinder (NLet t v)
190− = do (tv, tt) <- chk u env t
222+ = do (tv, tt) <- chk u maxu env t
191− (vv, vt) <- chk u env v
223+ (vv, vt) <- chk u maxu env v
192 let tv' = normalise ctxt env tv
224 let tv' = normalise ctxt env tv
193 let tt' = normalise ctxt env tt
225 let tt' = normalise ctxt env tt
194 convertsC ctxt env vt tv
226 convertsC ctxt env vt tv
@@ -197,13 +229,13 @@ check' holes ctxt env top = chk (TType (UVar (-5))) env top where
197 checkBinder (Hole t)
229 checkBinder (Hole t)
198 | not holes = lift $ tfail (IncompleteTerm undefined)
230 | not holes = lift $ tfail (IncompleteTerm undefined)
199 | otherwise
231 | otherwise
200− = do (tv, tt) <- chk u env t
232+ = do (tv, tt) <- chk u maxu env t
201 let tv' = normalise ctxt env tv
233 let tv' = normalise ctxt env tv
202 let tt' = normalise ctxt env tt
234 let tt' = normalise ctxt env tt
203 lift $ isType ctxt env tt'
235 lift $ isType ctxt env tt'
204 return (Hole tv, tt')
236 return (Hole tv, tt')
205 checkBinder (GHole i t)
237 checkBinder (GHole i t)
206− = do (tv, tt) <- chk u env t
238+ = do (tv, tt) <- chk u maxu env t
207 let tv' = normalise ctxt env tv
239 let tv' = normalise ctxt env tv
208 let tt' = normalise ctxt env tt
240 let tt' = normalise ctxt env tt
209 lift $ isType ctxt env tt'
241 lift $ isType ctxt env tt'
@@ -211,15 +243,15 @@ check' holes ctxt env top = chk (TType (UVar (-5))) env top where
211 checkBinder (Guess t v)
243 checkBinder (Guess t v)
212 | not holes = lift $ tfail (IncompleteTerm undefined)
244 | not holes = lift $ tfail (IncompleteTerm undefined)
213 | otherwise
245 | otherwise
214− = do (tv, tt) <- chk u env t
246+ = do (tv, tt) <- chk u maxu env t
215− (vv, vt) <- chk u env v
247+ (vv, vt) <- chk u maxu env v
216 let tv' = normalise ctxt env tv
248 let tv' = normalise ctxt env tv
217 let tt' = normalise ctxt env tt
249 let tt' = normalise ctxt env tt
218 convertsC ctxt env vt tv
250 convertsC ctxt env vt tv
219 lift $ isType ctxt env tt'
251 lift $ isType ctxt env tt'
220 return (Guess tv vv, tt')
252 return (Guess tv vv, tt')
221 checkBinder (PVar t)
253 checkBinder (PVar t)
222− = do (tv, tt) <- chk u env t
254+ = do (tv, tt) <- chk u maxu env t
223 let tv' = normalise ctxt env tv
255 let tv' = normalise ctxt env tv
224 let tt' = normalise ctxt env tt
256 let tt' = normalise ctxt env tt
225 lift $ isType ctxt env tt'
257 lift $ isType ctxt env tt'
@@ -227,7 +259,7 @@ check' holes ctxt env top = chk (TType (UVar (-5))) env top where
227 -- to tell if it's a collapsible variable)
259 -- to tell if it's a collapsible variable)
228 return (PVar tv, tt')
260 return (PVar tv, tt')
229 checkBinder (PVTy t)
261 checkBinder (PVTy t)
230− = do (tv, tt) <- chk u env t
262+ = do (tv, tt) <- chk u maxu env t
231 let tv' = normalise ctxt env tv
263 let tv' = normalise ctxt env tv
232 let tt' = normalise ctxt env tt
264 let tt' = normalise ctxt env tt
233 lift $ isType ctxt env tt'
265 lift $ isType ctxt env tt'
src/Idris/Elab/Data.hs+13−4
@@ -64,7 +64,7 @@ elabData info syn doc argDocs fc opts (PDatadecl n t_in dcons)
64 = do let codata = Codata `elem` opts
64 = do let codata = Codata `elem` opts
65 iLOG (show fc)
65 iLOG (show fc)
66 undef <- isUndefined fc n
66 undef <- isUndefined fc n
67− (cty, _, t, inacc) <- buildType info syn fc [] n t_in
67+ (cty, ckind, t, inacc) <- buildType info syn fc [] n t_in
68 -- if n is defined already, make sure it is just a type declaration
68 -- if n is defined already, make sure it is just a type declaration
69 -- with the same type we've just elaborated, and no constructors
69 -- with the same type we've just elaborated, and no constructors
70 -- yet
70 -- yet
@@ -76,7 +76,7 @@ elabData info syn doc argDocs fc opts (PDatadecl n t_in dcons)
76 let unique = case getRetTy cty of
76 let unique = case getRetTy cty of
77 UType UniqueType -> True
77 UType UniqueType -> True
78 _ -> False
78 _ -> False
79− cons <- mapM (elabCon cnameinfo syn n codata (getRetTy cty)) dcons
79+ cons <- mapM (elabCon cnameinfo syn n codata (getRetTy cty) ckind) dcons
80 ttag <- getName
80 ttag <- getName
81 i <- getIState
81 i <- getIState
82 let as = map (const (Left (Msg ""))) (getArgTys cty)
82 let as = map (const (Left (Msg ""))) (getArgTys cty)
@@ -210,16 +210,18 @@ elabData info syn doc argDocs fc opts (PDatadecl n t_in dcons)
210 }
210 }
211
211
212elabCon :: ElabInfo -> SyntaxInfo -> Name -> Bool ->
212elabCon :: ElabInfo -> SyntaxInfo -> Name -> Bool ->
213− Type -> -- for kind checking
213+ Type -> -- for unique kind checking
214+ Type -> -- data type's kind
214 (Docstring (Either Err PTerm), [(Name, Docstring (Either Err PTerm))], Name, PTerm, FC, [Name]) ->
215 (Docstring (Either Err PTerm), [(Name, Docstring (Either Err PTerm))], Name, PTerm, FC, [Name]) ->
215 Idris (Name, Type)
216 Idris (Name, Type)
216−elabCon info syn tn codata expkind (doc, argDocs, n, t_in, fc, forcenames)
217+elabCon info syn tn codata expkind dkind (doc, argDocs, n, t_in, fc, forcenames)
217 = do checkUndefined fc n
218 = do checkUndefined fc n
218 logLvl 2 $ show fc ++ ":Constructor " ++ show n ++ " : " ++ show t_in
219 logLvl 2 $ show fc ++ ":Constructor " ++ show n ++ " : " ++ show t_in
219 (cty, ckind, t, inacc) <- buildType info syn fc [Constructor] n (if codata then mkLazy t_in else t_in)
220 (cty, ckind, t, inacc) <- buildType info syn fc [Constructor] n (if codata then mkLazy t_in else t_in)
220 ctxt <- getContext
221 ctxt <- getContext
221 let cty' = normalise ctxt [] cty
222 let cty' = normalise ctxt [] cty
222 checkUniqueKind ckind expkind
223 checkUniqueKind ckind expkind
224+ addDataConstraint ckind dkind
223
225
224 -- Check that the constructor type is, in fact, a part of the family being defined
226 -- Check that the constructor type is, in fact, a part of the family being defined
225 tyIs n cty'
227 tyIs n cty'
@@ -280,6 +282,13 @@ elabCon info syn tn codata expkind (doc, argDocs, n, t_in, fc, forcenames)
280 checkUniqueKind (UType AllTypes) _ = return ()
282 checkUniqueKind (UType AllTypes) _ = return ()
281 checkUniqueKind _ _ = return ()
283 checkUniqueKind _ _ = return ()
282
284
285+ -- Constructor's kind must be <= expected kind
286+ addDataConstraint (TType con) (TType exp)
287+ = do ctxt <- getContext
288+ let v = next_tvar ctxt
289+ addConstraints fc (v, [ULT con exp])
290+ addDataConstraint _ _ = return ()
291+
283type EliminatorState = StateT (Map.Map String Int) Idris
292type EliminatorState = StateT (Map.Map String Int) Idris
284
293
285-- -- Issue #1616 in the issue tracker.
294-- -- Issue #1616 in the issue tracker.
test/error001/expected+5−6
@@ -1,10 +1,9 @@
1test002.idr:5:6:Universe inconsistency.
1test002.idr:5:6:Universe inconsistency.
2−Working on: f2
2+Working on: e2
3−Old domain: Domain 7 7
3+Old domain: Domain 4 4
4−New domain: Domain 7 6
4+New domain: Domain 4 3
5Involved constraints:
5Involved constraints:
6− (f2 <= i1,test002.idr:5:6)
7 (e2 < f2,test002.idr:5:6)
6 (e2 < f2,test002.idr:5:6)
8− (j1 <= f2,test002.idr:5:6)
7+ (e2 < f2,test002.idr:5:6)
9− (f2 <= i1,test002.idr:5:6)
8+ (i1 <= e2,test002.idr:5:6)
10
9