GitLab

I'm not sure whether it is a bug, but there have been two recent reports of ghc-7.2.1 not treating type constructor variables as injective. First, by Daniel Schüssler,

{-# LANGUAGE GADTs, TypeOperators, TypeFamilies, ScopedTypeVariables #-}
module DTest where

data a :=: b where 
    Refl :: a :=: a

subst :: a :=: b -> f a -> f b
subst Refl = id 

-- Then this doesn't work (error message at the bottom):

inj1 :: forall f a b. f a :=: f b -> a :=: b
inj1 Refl = Refl

-- But one can still construct it with a trick that Oleg used in the context of 
-- Leibniz equality:

type family Arg fa

type instance Arg (f a) = a

newtype Helper fa fa' = Helper { runHelper :: Arg fa :=: Arg fa' }

inj2 :: forall f a b. f a :=: f b -> a :=: b
inj2 p = runHelper (subst p (Helper Refl :: Helper (f a) (f a)))

{-
DTest.hs:13:13:
    Could not deduce (a ~ b)
    from the context (f a ~ f b)
      bound by a pattern with constructor
                 Refl :: forall a. a :=: a,
               in an equation for `inj1'
      at DTest.hs:13:6-9
      `a' is a rigid type variable bound by
          the type signature for inj1 :: (f a :=: f b) -> a :=: b
          at DTest.hs:13:1
      `b' is a rigid type variable bound by
          the type signature for inj1 :: (f a :=: f b) -> a :=: b
          at DTest.hs:13:1
    Expected type: a :=: b
      Actual type: a :=: a
    In the expression: Refl
    In an equation for `inj1': inj1 Refl = Refl
-}

compiles fine with ghc-7.0.4. Second, by Sjoerd Visscher,

{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, KindSignatures, 
    GADTs, FlexibleInstances, FlexibleContexts #-}
module STest where

class Monad m => Effect p e r m | p e m -> r where
  fin :: p e m -> e -> m r

data ErrorEff :: * -> (* -> *) -> * where 
  CatchError :: (e -> m a) -> ErrorEff ((e -> m a) -> m a) m

instance Monad m => Effect ErrorEff ((e -> m a) -> m a) a m where
  fin (CatchError h) = \f -> f h

{-
STest.hs:12:32:
    Could not deduce (a1 ~ a)
    from the context (Monad m)
      bound by the instance declaration at STest.hs:11:10-59
    or from (((e -> m a) -> m a) ~ ((e1 -> m a1) -> m a1))
      bound by a pattern with constructor
                 CatchError :: forall (m :: * -> *) e a.
                               (e -> m a) -> ErrorEff ((e -> m a) -> m a) m,
               in an equation for `fin'
      at STest.hs:12:8-19
      `a1' is a rigid type variable bound by
           a pattern with constructor
             CatchError :: forall (m :: * -> *) e a.
                           (e -> m a) -> ErrorEff ((e -> m a) -> m a) m,
           in an equation for `fin'
           at STest.hs:12:8
      `a' is a rigid type variable bound by
          the instance declaration at STest.hs:11:46
    Expected type: e1 -> m a1
      Actual type: e -> m a
    In the first argument of `f', namely `h'
    In the expression: f h
-}

also compiles fine with 7.0.4. ghc-7.3.20111026 behaves like 7.2.1. Which version behaves correctly?

Trac metadata

Trac field	Value
Version	7.2.1
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler (Type checker)
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture