#7176: Failure to let kind variable remain uninstantiated when not needed
------------------------------+---------------------------------------------
Reporter: goldfire | Owner:
Type: bug | Status: new
Priority: normal | Component: Compiler
Version: 7.6.1-rc1 | Keywords: PolyKinds TypeFamilies
Os: Unknown/Multiple | Architecture: Unknown/Multiple
Failure: None/Unknown | Testcase:
Blockedby: | Blocking:
Related: |
------------------------------+---------------------------------------------
Consider the following code:
{{{
{-# LANGUAGE TypeFamilies, DataKinds, PolyKinds, GADTs, RankNTypes #-}
type family Sing (a :: b)
data SMaybe (a :: Maybe c) where
SNothing :: SMaybe Nothing
SJust :: Sing a -> SMaybe (Just a)
type instance Sing (a :: Maybe d) = SMaybe a
sIsJust :: forall (a :: Maybe e). Sing a -> ()
sIsJust SNothing = ()
sIsJust (SJust _) = ()
}}}
Compiling produces the following error twice on the first part of the type
of {{{sIsJust}}}:
{{{
Couldn't match kind `k1' with `e'
because type variable `e' would escape its scope
This (rigid, skolem) type variable is bound by
the type signature for sIsJust :: Sing (Maybe e) a -> ()
Expected type: Sing (Maybe e) a
Actual type: SMaybe k1 a
}}}
I'm not 100% convinced that this is an error in GHC, but it would seem to
me that {{{sIsJust}}} should compile. The explicit quantification is
necessary to fix the kind of {{{a}}}, which allows {{{Sing a}}} to
simplify to {{{SMaybe a}}}.
My guideline for why this should compile is that the following compiles
without complaint:
{{{
type family F a
type instance F a = [a]
foo :: F a -> ()
foo [] = ()
foo (_:_) = ()
}}}
--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/7176>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
_______________________________________________
Glasgow-haskell-bugs mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
