#7973: Simplifier introduces unbound kind variables (caught by -dcore-lint)
-----------------------------+----------------------------------------------
Reporter: diatchki | Owner:
Type: bug | Status: new
Priority: normal | Component: Compiler (Type checker)
Version: 7.7 | Keywords:
Os: Unknown/Multiple | Architecture: Unknown/Multiple
Failure: None/Unknown | Blockedby:
Blocking: | Related:
-----------------------------+----------------------------------------------
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 core-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).