Type constructor variables not injective
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 |