diff options
| author | Simon Peyton Jones <simonpj@microsoft.com> | 2012-09-18 17:32:42 +0100 |
|---|---|---|
| committer | Simon Peyton Jones <simonpj@microsoft.com> | 2012-09-18 17:32:42 +0100 |
| commit | 19dd108cd15ab3d0cc538903217eef9be54a02e5 (patch) | |
| tree | ed1a6540ec08cd17847caa28ea261fef50e2cbc0 /compiler | |
| parent | 1b5c8337577eea64972856b0466a7fbc36683540 (diff) | |
| download | haskell-19dd108cd15ab3d0cc538903217eef9be54a02e5.tar.gz | |
Be careful about kinds when eta-expanding AppCo
See Note [Eta for AppCo] in OptCoercion
Diffstat (limited to 'compiler')
| -rw-r--r-- | compiler/types/OptCoercion.lhs | 27 |
1 files changed, 25 insertions, 2 deletions
diff --git a/compiler/types/OptCoercion.lhs b/compiler/types/OptCoercion.lhs index c699163e74..a039fe5b3f 100644 --- a/compiler/types/OptCoercion.lhs +++ b/compiler/types/OptCoercion.lhs @@ -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 + |