[GHC] #12021: Type variable escapes its scope

[GHC]

#12021: Type variable escapes its scope
-------------------------------------+-------------------------------------
           Reporter:  ttuegel        |             Owner:
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.0.1-rc3
           Keywords:                 |  Operating System:  Linux
       Architecture:  x86_64         |   Type of failure:  GHC rejects
  (amd64)                            |  valid program
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 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
 {{{#!hs
 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
 {{{#!hs
 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.)

 {{{#!hs
 {-# 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)
 }}}

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12021>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler