#5591: Type constructor variables not injective
----------------------------------+-----------------------------------------
Reporter: daniel.is.fischer | Owner:
Type: bug | Status: new
Priority: normal | Component: Compiler (Type checker)
Version: 7.2.1 | Keywords:
Testcase: | Blockedby:
Os: Unknown/Multiple | Blocking:
Architecture: Unknown/Multiple | Failure: None/Unknown
----------------------------------+-----------------------------------------
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 [http://haskell.org/pipermail/haskell-cafe/2011-October/096221.html
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
[http://stackoverflow.com/questions/7866375/why-does-ghc-think-that-this-
type-variable-is-not-injective 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?
--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/5591>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
_______________________________________________
Glasgow-haskell-bugs mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
