#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). <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 }}} -- Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/7973> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler