GitLab

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