Opened 3 years ago
Closed 2 years ago
#9211 closed bug (fixed)
Untouchable type variable (regression from 7.6)
Reported by: | simonpj | Owned by: | |
---|---|---|---|
Priority: | normal | Milestone: | |
Component: | Compiler | Version: | 7.8.2 |
Keywords: | Cc: | oleg@…, dimitris@… | |
Operating System: | Unknown/Multiple | Architecture: | Unknown/Multiple |
Type of failure: | None/Unknown | Test Case: | indexed-types/should_compile/T9211 |
Blocked By: | Blocking: | ||
Related Tickets: | Differential Rev(s): | ||
Wiki Page: |
Description
Oleg says: what used to type check in GHC 7.4.1 (and I think in 7.6.2, although I no longer have access to that version) fails in GHC 7.8.2.
The following program type-checks with GHC 7.4.1 and GHC 7.8.2:
{-# LANGUAGE RankNTypes #-} {-# LANGUAGE TypeFamilies #-} module T where foo :: (forall f g. (Functor f) => f a -> f b) -> [a] -> [b] -- foo :: (forall f g. (Functor f, g ~ f) => g a -> g b) -> [a] -> [b] foo tr x = tr x t = foo (fmap not) [True]
The following code (which differs only in the signature of foo)
{-# LANGUAGE RankNTypes #-} {-# LANGUAGE TypeFamilies #-} module T where -- foo :: (forall f g. (Functor f) => f a -> f b) -> [a] -> [b] foo :: (forall f g. (Functor f, g ~ f) => g a -> g b) -> [a] -> [b] foo tr x = tr x t = foo (fmap not) [True]
type-checks with 7.4.1 but not with 7.8.2. The latter reports the error
Couldn't match type `b' with `Bool' `b' is untouchable inside the constraints (Functor f, g ~ f) bound by a type expected by the context: (Functor f, g ~ f) => g Bool -> g b at /tmp/t.hs:12:5-25 `b' is a rigid type variable bound by the inferred type of t :: [b] at /tmp/t.hs:12:1 Expected type: Bool -> b Actual type: Bool -> Bool Relevant bindings include t :: [b] (bound at /tmp/t.hs:12:1) In the first argument of `fmap', namely `not' In the first argument of `foo', namely `(fmap not)'
Giving t
the type signature [Bool]
fixes the problem. Alas, I come across the similar untouchable error in situations where giving the type signature is quite difficult (in local bindings, with quite large types).
Change History (10)
comment:1 Changed 3 years ago by
Cc: | oleg@… added |
---|
comment:2 Changed 3 years ago by
comment:3 Changed 3 years ago by
Upcoming partial type signatures and/or explicit type application will help, but these are both some distance away.
comment:4 Changed 3 years ago by
My real examples are not that different from the one I posted. Here is one of the recent ones:
unsafeLam :: (Applicative m, AppPermutable i, SSym repr, LamPure repr) => (forall j. (j ~ (->) (repr a))) => (i :. j) (repr a) -> (m :. (i :. j)) (repr b)) -> (m :. i) (repr (a->b))
As you can see, I use the type equality constraint to give an abbreviation to a complex type that appears several times in a complex expression. In the above example, 'j' is used as an abbreviation for '(->) (repr a)' that occurs twice in a large type. OCaml has the convenient notation 'type as x -> x -> x' to give an abbreviation to a type. I was happy that I found something similar in Haskell. Alas, as this ticket shows, sometimes it doesn't work. I have fixed my problem by getting rid of the abbreviation. (Giving the local type annotation in the real case proved to be too messy. The compiler kept complaining and needing more and more annotations.)
comment:5 Changed 3 years ago by
Cc: | dimitris@… added |
---|
Harumph.
Suppose we have an implication constraint of this form:
forall a b c. (b ~ ty, ...) => ...blah...
where the equality constraint in the "givens" is of form b ~ ty
, where b
is one of the variables quantified by the forall
.
Then, as far as I can see, no loss of principality arises if we float constraints from ...blah...
, outside the implication. (Obviously, only ones that do not mention a,b,c
.) (NB: floating the constraint out is equivalent to allowing a unification of an untouchable underneath.)
Reason: such an equality amounts to a let-binding; indeed that is exactly how Oleg wants to use it.
This would amount to an ad-hoc but easily-specified extension of GHC's already-ad-hoc rule for floating constraints out of implications, and hence perhaps no big deal. Certainly it's easy to implement.
I'm adding Dimitrios in cc. What do you think?
Simon
comment:6 Changed 3 years ago by
Indeed I use the equality constraint to essentially let-bind a type variable, which is quite handy. I'm glad to hear that it is also easy to implement. I, too, am curious what Dimitrios thinks.
comment:7 Changed 3 years ago by
Notes from S and D
- Level on skols
- Orient skol eqs a~b
- Level on EqCtList
- getUnsolvedInerts also looks for given equalities FROM THIS LEVEL
- …and finds non-let-bound ones
Let-bound ones
- a~ty, where a is a skol from this level
- F tys ~ b, where b is a skol from this level, and b does not appear in any remaining ones
(iterate)
comment:10 Changed 2 years ago by
Resolution: | → fixed |
---|---|
Status: | new → closed |
Test Case: | → indexed-types/should_compile/T9211 |
This looks right to me, and 7.4 looks wrong. There really is an equality
(f ~ g)
in the context, and so it's in general unsafe to fixb
toBool
. That's what the OutsideIn paper is all about.In this case the equality is trivial but presumably it's not trivial in your real example.
For a trivial equality like this, perhaps GHC is over-conservative, but lifting that would require yet more special-case pleading. And I'm not sure it'd fix your real example anyway.
In short, I don't know how to help.
Simon