Failure to let kind variable remain uninstantiated when not needed
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 (_:_) = ()
Trac metadata
Trac field | Value |
---|---|
Version | 7.6.1-rc1 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | |
Operating system | |
Architecture |