Commit 19dd108c authored by Simon Peyton Jones's avatar Simon Peyton Jones
Browse files

Be careful about kinds when eta-expanding AppCo

See Note [Eta for AppCo] in OptCoercion
parent 1b5c8337
......@@ -391,8 +391,9 @@ etaAppCo_maybe co
| Just (co1,co2) <- splitAppCo_maybe co
= Just (co1,co2)
| Pair ty1 ty2 <- coercionKind co
, Just {} <- splitAppTy_maybe ty1
, Just {} <- splitAppTy_maybe ty2
, Just (_,t1) <- splitAppTy_maybe ty1
, Just (_,t2) <- splitAppTy_maybe ty2
, typeKind t1 `eqType` typeKind t2 -- Note [Eta for AppCo]
= Just (LRCo CLeft co, LRCo CRight co)
| otherwise
= Nothing
......@@ -421,3 +422,25 @@ etaTyConAppCo_maybe tc co
| otherwise
= Nothing
\end{code}
Note [Eta for AppCo]
~~~~~~~~~~~~~~~~~~~~
Supopse we have
g :: s1 t1 ~ s2 t2
Then we can't necessarily make
left g :: s1 ~ s2
right g :: t1 ~ t2
becuase it's poossible that
s1 :: * -> * t1 :: *
s2 :: (*->*) -> * t2 :: * -> *
and in that case (left g) does not have the same
kind on either side.
It's enough to check that
kind t1 = kind t2
because if g is well-kinded then
kind (s1 t2) = kind (s2 t2)
and these two imply
kind s1 = kind s2
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment