Opened 5 years ago

Closed 4 years ago

Last modified 4 years ago

#7176 closed bug (fixed)

Failure to let kind variable remain uninstantiated when not needed

Reported by: goldfire Owned by:
Priority: normal Milestone:
Component: Compiler Version: 7.6.1-rc1
Keywords: PolyKinds TypeFamilies Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case: polykinds/T7176
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:


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 (_:_) = ()

Change History (4)

comment:1 Changed 5 years ago by simonpj

difficulty: Unknown

Aha. I have fixed this on the 7.6 branch thus:

commit 5133bb97a47340a9008615e412fcf62f7762bea8
Author: Simon Peyton Jones <>
Date:   Wed Aug 22 18:01:57 2012 +0100

    Allocate a fresh META unique in newMetaKindVar
    Fixes Trac #7176 on the branch.  HEAD has a better fix
    (the big patch to untouchable handling)

 compiler/typecheck/TcMType.lhs |    2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

Separate fix for HEAD coming

comment:2 Changed 4 years ago by simonpj

Resolution: fixed
Status: newclosed
Test Case: polykinds/T7176

comment:3 Changed 4 years ago by simonpj

In the end I did the same tiny fix on the HEAD, to avoid getting tangled up in later changes

commit f4c327ad08d9df0fbafa0ad476a9ef26f8cd6abb
Author: Simon Peyton Jones <>
Date:   Fri Sep 14 11:12:01 2012 +0100

    When allocating a new kind variable, do so with newMetaUnique


 compiler/typecheck/TcMType.lhs |    2 +-
 1 files changed, 1 insertions(+), 1 deletions(-)

diff --git a/compiler/typecheck/TcMType.lhs b/compiler/typecheck/TcMType.lhs index a212f25..67ed967 100644
--- a/compiler/typecheck/TcMType.lhs
+++ b/compiler/typecheck/TcMType.lhs
@@ -113,7 +113,7 @@ import Data.List        ( (\\), partition, mapAccumL )
 newMetaKindVar :: TcM TcKind
-newMetaKindVar = do { uniq <- newUnique
+newMetaKindVar = do { uniq <- newMetaUnique
 		    ; ref <- newMutVar Flexi
 		    ; return (mkTyVarTy (mkMetaKindVar uniq ref)) }

comment:4 Changed 4 years ago by simonpj@…

commit 1128f1e02ff06fee89b62fb756ac0c28edcf4625

Author: Simon Peyton Jones <>
Date:   Wed Apr 3 14:37:50 2013 +0100

    This changes fixes a bad error in canonicalisation, concerning kind equality
    We care careful not to construct a canonical equality whose LHS and RHS
    have incompatible kinds.  (This is one of the invariants of a canonical
    equality.)  See Note [Equalities with incompatible kinds].  However,
    what I had not dealt with is when LHS and RHS *look* as if they have
    different kinds, but after zonking they become the same.  Bad!
    (This led to an ASSERT failure in the test for Trac #7176.)

 compiler/typecheck/TcCanonical.lhs |  111 +++++++++++++++++++++---------------
 1 files changed, 65 insertions(+), 46 deletions(-)
Note: See TracTickets for help on using tickets.