Simplifier introduces unbound kind variables (caught by -dcore-lint)
I encountered a problem in GHC (happens with 7.6.3 and HEAD), where compiling with optimizations (-O2) results in invalid core (unbound kind variable).
I managed to reduce my example to the following:
{-# LANGUAGE DataKinds, PolyKinds, KindSignatures #-}
{-# LANGUAGE ExistentialQuantification, UndecidableInstances, TypeFamilies #-}
module Test where
-- Kind-level proxies.
data {-kind-} K (a :: *) = KP
-- A type with 1 kind-polymorphic type argument.
data T (n :: k)
-- A type with 1 kind argument.
data F (kp :: K k)
-- A class with 1 kind argument.
class (kp ~ KP) => C (kp :: K k) where
f :: T (a :: k) -> F kp
-- A type with 1 kind argument.
-- Contains an existentially quantified type-variable of this kind.
data SomeT (kp :: K k) = forall (n :: k). Mk (T n)
-- Show `SomeT` by converting it to `F`, using `C`.
instance (C kp, Show (F kp)) => Show (SomeT kp) where
show (Mk x) = show (f x)
I compiled it with these flags:
ghc-stage2 -c -O2 -dcore-lint test.hs
Part of the cire-lint complaint is:
*** Core Lint errors : in result of Simplifier ***
<no location info>: Warning:
In the expression: ww_snF
@ n_akd
(x_aie
`cast` (Sym
(Nth:0
((forall (a_ai7 :: k_aj7).
<Test.T k_ajF a_ai7> -> Test.F <k_ajF> cobox_dkK)@n_akd))
:: Test.T k_ajF n_akd ~# Test.T k_ajF n_akd))
@ (k_aj7 :: BOX) is out of scope
Trac metadata
Trac field | Value |
---|---|
Version | 7.7 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler (Type checker) |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | |
Operating system | |
Architecture |