git.iko.soy/Idris-dev
on master help sign in
Merge pull request #1685 from soimort/fix-checkUniqueKind
5161784Edwin Brady
src/Idris/Elab/Data.hs+2−2
compare with master
unifiedsplit
@@ -265,10 +265,10 @@ elabCon info syn tn codata expkind (doc, argDocs, n, t_in, fc, forcenames)
265 = tclift $ tfail (At fc (UniqueKindError NullType n))
265 = tclift $ tfail (At fc (UniqueKindError NullType n))
266 checkUniqueKind (UType UniqueType) (UType UniqueType) = return ()
266 checkUniqueKind (UType UniqueType) (UType UniqueType) = return ()
267 checkUniqueKind (UType UniqueType) (UType AllTypes) = return ()
267 checkUniqueKind (UType UniqueType) (UType AllTypes) = return ()
268− checkUniqueKind (UType UniqueType) (TType _)
268+ checkUniqueKind (UType UniqueType) _
269 = tclift $ tfail (At fc (UniqueKindError UniqueType n))
269 = tclift $ tfail (At fc (UniqueKindError UniqueType n))
270 checkUniqueKind (UType AllTypes) _ = return ()
270 checkUniqueKind (UType AllTypes) _ = return ()
271− checkUniqueKind (TType _) _ = return ()
271+ checkUniqueKind _ _ = return ()
272
272
273type EliminatorState = StateT (Map.Map String Int) Idris
273type EliminatorState = StateT (Map.Map String Int) Idris
274
274