Skip to content
Snippets Groups Projects
Commit 62d3fdeb authored by Richard Eisenberg's avatar Richard Eisenberg
Browse files

Allow non-Nominal covars (bugfix)

parent be7f10bb
No related branches found
No related tags found
No related merge requests found
...@@ -802,7 +802,7 @@ isReflCo_maybe _ = Nothing ...@@ -802,7 +802,7 @@ isReflCo_maybe _ = Nothing
mkCoVarCo :: CoVar -> Coercion mkCoVarCo :: CoVar -> Coercion
-- cv :: s ~# t -- cv :: s ~# t
mkCoVarCo cv mkCoVarCo cv
| ty1 `eqType` ty2 = Refl Nominal ty1 | ty1 `eqType` ty2 = Refl (coVarRole cv) ty1
| otherwise = CoVarCo cv | otherwise = CoVarCo cv
where where
(ty1, ty2) = ASSERT( isCoVar cv ) coVarKind cv (ty1, ty2) = ASSERT( isCoVar cv ) coVarKind cv
...@@ -1360,8 +1360,7 @@ subst_co subst co ...@@ -1360,8 +1360,7 @@ subst_co subst co
substCoVar :: CvSubst -> CoVar -> Coercion substCoVar :: CvSubst -> CoVar -> Coercion
substCoVar (CvSubst in_scope _ cenv) cv substCoVar (CvSubst in_scope _ cenv) cv
| Just co <- lookupVarEnv cenv cv = ASSERT2( coercionRole co == Nominal, ppr co ) | Just co <- lookupVarEnv cenv cv = co
co
| Just cv1 <- lookupInScope in_scope cv = ASSERT( isCoVar cv1 ) CoVarCo cv1 | Just cv1 <- lookupInScope in_scope cv = ASSERT( isCoVar cv1 ) CoVarCo cv1
| otherwise = WARN( True, ptext (sLit "substCoVar not in scope") <+> ppr cv $$ ppr in_scope) | otherwise = WARN( True, ptext (sLit "substCoVar not in scope") <+> ppr cv $$ ppr in_scope)
ASSERT( isCoVar cv ) CoVarCo cv ASSERT( isCoVar cv ) CoVarCo cv
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment