[GHC] #9211: Untouchable type variable (regression from 7.6)
#9211: Untouchable type variable (regression from 7.6) ------------------------------------+------------------------------------- Reporter: simonpj | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 Keywords: | Operating System: Unknown/Multiple Architecture: Unknown/Multiple | Type of failure: None/Unknown Difficulty: Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | ------------------------------------+------------------------------------- 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). -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/9211> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#9211: Untouchable type variable (regression from 7.6) -------------------------------------+------------------------------------ Reporter: simonpj | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Changes (by simonpj): * cc: oleg@… (added) -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/9211#comment:1> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#9211: Untouchable type variable (regression from 7.6) -------------------------------------+------------------------------------ Reporter: simonpj | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (by simonpj): 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 -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/9211#comment:2> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#9211: Untouchable type variable (regression from 7.6) -------------------------------------+------------------------------------ Reporter: simonpj | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (by goldfire): Upcoming partial type signatures and/or explicit type application will help, but these are both some distance away. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/9211#comment:3> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#9211: Untouchable type variable (regression from 7.6) -------------------------------------+------------------------------------ Reporter: simonpj | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (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.) -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/9211#comment:4> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#9211: Untouchable type variable (regression from 7.6) -------------------------------------+------------------------------------ Reporter: simonpj | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Changes (by simonpj): * cc: dimitris@… (added) Comment: 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 -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/9211#comment:5> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#9211: Untouchable type variable (regression from 7.6) -------------------------------------+------------------------------------ Reporter: simonpj | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (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. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/9211#comment:6> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#9211: Untouchable type variable (regression from 7.6) -------------------------------------+------------------------------------- Reporter: simonpj | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 Resolution: | Keywords: Operating System: | Architecture: Unknown/Multiple Unknown/Multiple | Difficulty: Unknown Type of failure: | Blocked By: None/Unknown | Related Tickets: Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (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) -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/9211#comment:7> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#9211: Untouchable type variable (regression from 7.6) -------------------------------------+------------------------------------- Reporter: simonpj | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 Resolution: | Keywords: Operating System: | Architecture: Unknown/Multiple Unknown/Multiple | Difficulty: Unknown Type of failure: | Blocked By: None/Unknown | Related Tickets: Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (by Simon Peyton Jones <simonpj@…>): In [changeset:"5770029a1f8509a673b2277287fc8fe90b9b6002/ghc"]: {{{ #!CommitTicketReference repository="ghc" revision="5770029a1f8509a673b2277287fc8fe90b9b6002" Simon's major commit to re-engineer the constraint solver The driving change is this: * The canonical CFunEqCan constraints now have the form [G] F xis ~ fsk [W] F xis ~ fmv where fsk is a flatten-skolem, and fmv is a flatten-meta-variable Think of them as the name of the type-function application See Note [The flattening story] in TcFlatten. A flatten-meta-variable is distinguishable by its MetaInfo of FlatMetaTv This in turn led to an enormous cascade of other changes, which simplify and modularise the constraint solver. In particular: * Basic data types * I got rid of inert_solved_funeqs altogether. It serves no useful role that inert_flat_cache does not solve. * I added wl_implics to the WorkList, as a convenient place to accumulate newly-emitted implications; see Note [Residual implications] in TcSMonad. * I eliminated tcs_ty_binds altogether. These were the bindings for unification variables that we have now solved by unification. We kept them in a finite map and did the side-effecting unification later. But in cannonicalisation we had to look up in the side-effected mutable tyvars anyway, so nothing was being gained. Our original idea was that the solver would be pure, and would be a no-op if you discarded its results, but this was already not-true for implications since we update their evidence bindings in an imperative way. So rather than the uneasy compromise, it's now clearly imperative! * I split out the flatten/unflatten code into a new module, TcFlatten * I simplified and articulated explicitly the (rather hazy) invariants for the inert substitution inert_eqs. See Note [eqCanRewrite] and See Note [Applying the inert substitution] in TcFlatten * Unflattening is now done (by TcFlatten.unflatten) after solveFlats, before solving nested implications. This turned out to simplify a lot of code. Previously, unflattening was done as part of zonking, at the very very end. * Eager unflattening allowed me to remove the unpleasant ic_fsks field of an Implication (hurrah) * Eager unflattening made the TcSimplify.floatEqualities function much simpler (just float equalities looking like a ~ ty, where a is an untouchable meta-tyvar). * Likewise the idea of "pushing wanteds in as givens" could be completely eliminated. * I radically simplified the code that determines when there are 'given' equalities, and hence whether we can float 'wanted' equalies out. See TcSMonad.getNoGivenEqs, and Note [When does an implication have given equalities?]. This allowed me to get rid of the unpleasant inert_no_eqs flag in InertCans. * As part of this given-equality stuff, I fixed Trac #9211. See Note [Let-bound skolems] in TcSMonad * Orientation of tyvar/tyvar equalities (a ~ b) was partly done during canonicalisation, but then repeated in the spontaneous-solve stage (trySpontaneousSolveTwoWay). Now it is done exclusively during canonicalisation, which keeps all the code in one place. See Note [Canonical orientation for tyvar/tyvar equality constraints] in TcCanonical }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/9211#comment:9> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#9211: Untouchable type variable (regression from 7.6) -------------------------------------+------------------------------------- Reporter: simonpj | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 Resolution: | Keywords: Operating System: | Architecture: Unknown/Multiple Unknown/Multiple | Difficulty: Unknown Type of failure: | Blocked By: None/Unknown | Related Tickets: Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (by Simon Peyton Jones <simonpj@…>): In [changeset:"4723a0e39b5eb7a47457696aceb67f8e230a42e6/ghc"]: {{{ #!CommitTicketReference repository="ghc" revision="4723a0e39b5eb7a47457696aceb67f8e230a42e6" Test Trac #9211 }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/9211#comment:8> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#9211: Untouchable type variable (regression from 7.6) -------------------------------------+------------------------------------- Reporter: simonpj | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 Resolution: fixed | Keywords: Operating System: | Architecture: Unknown/Multiple Unknown/Multiple | Difficulty: Unknown Type of failure: | Blocked By: None/Unknown | Related Tickets: Test Case: indexed- | types/should_compile/T9211 | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Changes (by simonpj): * status: new => closed * testcase: => indexed-types/should_compile/T9211 * resolution: => fixed -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/9211#comment:10> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
participants (1)
-
GHC