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 |