Opened 11 months ago
Closed 6 months 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 Revisions: |
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 11 months ago by simonpj
- Cc oleg@… added
comment:2 Changed 11 months ago by simonpj
comment:3 Changed 11 months ago by goldfire
Upcoming partial type signatures and/or explicit type application will help, but these are both some distance away.
comment:4 Changed 11 months ago by oleg
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 11 months ago by simonpj
- 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 11 months ago by oleg
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 9 months ago by simonpj
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:8 Changed 6 months ago by Simon Peyton Jones <simonpj@…>
comment:9 Changed 6 months ago by Simon Peyton Jones <simonpj@…>
comment:10 Changed 6 months ago by simonpj
- Resolution set to fixed
- Status changed from new to closed
- Test Case set to 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 fix b to Bool. 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