Type variable escapes its scope

In the following example, I believe a type variable is incorrectly escaping its scope. The example produces the error:

Bug.hs:20:20: error:
    • Expected kind ‘Cat k’,
        but ‘(:-)’ has kind ‘Constraint -> Constraint -> *’
    • In the first argument of ‘Iso’, namely ‘(:-)’
      In the type signature:
        functor :: forall a b.
                   Iso (:-) (:-) (Ob (Dom f) a) (Ob (Dom f) b) (Ob (Cod f) (f a)) (Ob (Cod f) (f b))
      In the class declaration for ‘Functor’

If the definition of Iso is changed from

type Iso (c :: Cat k) (d :: Cat k) s t a b =
    forall p. (Cod p ~ Nat d (->)) => p a b -> p s t

to

type Iso (c :: Cat k) (d :: Cat k) s t a b =
    forall p. p a b -> p s t

then this error does not occur. (The example still will not compile because I have omitted almost the entire implementation, but it should not fail here.)

I am not certain what is really happening here, but it seems to me that when the RHS of Iso is constrained, then the type variable k introduced on the LHS of Iso is being unified incorrectly with the type variable k introduced in the definition of the Functor class. When the constraint is removed, GHC seems to recognize (correctly!) that the type variables are distinct.

(This bug actually occurs with GHC 8.0.1-rc4, but the "Version" menu doesn't give me that option.)

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE NoImplicitPrelude #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}

import GHC.Base ( Constraint, Type )

type Cat k = k -> k -> Type

class Category (p :: Cat k) where
    type Ob p :: k -> Constraint

class (Category (Dom f), Category (Cod f)) => Functor (f :: j -> k) where
    type Dom f :: Cat j
    type Cod f :: Cat k
    functor :: forall a b.
               Iso (:-) (:-)
               (Ob (Dom f) a)     (Ob (Dom f) b)
               (Ob (Cod f) (f a)) (Ob (Cod f) (f b))

class (Functor f , Dom f ~ p, Cod f ~ q) =>
    Fun (p :: Cat j) (q :: Cat k) (f :: j -> k) | f -> p q
instance (Functor f , Dom f ~ p, Cod f ~ q) =>
    Fun (p :: Cat j) (q :: Cat k) (f :: j -> k)

data Nat (p :: Cat j) (q :: Cat k) (f :: j -> k) (g :: j -> k)

type Iso (c :: Cat k) (d :: Cat k) s t a b =
    forall p. (Cod p ~ Nat d (->)) => p a b -> p s t

data (p :: Constraint) :- (q :: Constraint)

Trac metadata

Trac field	Value
Version	8.0.1-rc3
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC	ghc-devs@haskell.org
Operating system
Architecture