#5591 closed bug (fixed)
Type constructor variables not injective
Reported by: | daniel.is.fischer | Owned by: | simonpj |
---|---|---|---|
Priority: | normal | Milestone: | 7.6.2 |
Component: | Compiler (Type checker) | Version: | 7.2.1 |
Keywords: | Cc: | dimitris@…, sweirich@…, byorgey@…, illissius@…, adam.gundry@…, andy.adamsmoran@… | |
Operating System: | Unknown/Multiple | Architecture: | Unknown/Multiple |
Type of failure: | None/Unknown | Test Case: | indexed-ypes/should_compile/T5591a, T5591b |
Blocked By: | Blocking: | ||
Related Tickets: | Differential Rev(s): | ||
Wiki Page: |
Description
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?
Change History (9)
comment:1 Changed 5 years ago by danielo
comment:2 Changed 5 years ago by simonpj
- Cc dimitris@… sweirich@… byorgey@… added
As Brent describes on StackOverflow, we did make a change that simplified GHC's internal language a bit, and allowed us to have unsaturated type functions. The change is described in 6.2 of our POPL'11 paper Generative type abstraction and type-level computation.
Daniel Shussler's email also describes a trick due to Oleg that makes his program compile. Well, it turns out that this trick is really a bug; with the restrictions describe in our paper, we should not allow type functions to match on an argument of shape (a b).
So far as we can all remember, the only reason for the new story was to allow un-saturated type functions in the intermediate language. But we can't allow them in the source language because that would mess up type inference. So we are paying the price (exemplified by this ticket) without getting much benefit.
Brent's conclusion on StackOverflow is that we should go back to
- having left and right coercion combinators
- requiring type functions to be saturated in the intermediate language (as well as source)
And that in turn would allow us to type check the program in this ticket.
So that's the plan I think. But gotta get 7.4 out first.
Simon
comment:3 Changed 5 years ago by igloo
- Milestone set to 7.6.1
- Owner set to simonpj
comment:4 Changed 4 years ago by illissius
- Cc illissius@… added
comment:5 Changed 4 years ago by simonpj
- difficulty set to Unknown
illissius, do you have an application in mind?
comment:6 Changed 4 years ago by adamgundry
- Cc adam.gundry@… added
comment:7 Changed 4 years ago by igloo
- Milestone changed from 7.6.1 to 7.6.2
comment:8 Changed 4 years ago by simonpj
- Resolution set to fixed
- Status changed from new to closed
- Test Case set to indexed-ypes/should_compile/T5591a, T5591b
Fixed at last; see #7205. I added both examples as regression tests.
Simon
comment:9 Changed 3 years ago by morabbin
- Cc andy.adamsmoran@… added
Is this related to #6018? Brent's stack overflow comment seems to imply it is.
I reduced second example, compiles in 7.0.3, but not in 7.3.20111021. Seems a serious shortcoming to me