Opened 5 years ago

Closed 5 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:


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 5 years ago by simonpj

Cc: oleg@… added

comment:2 Changed 5 years ago 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.


comment:3 Changed 5 years ago by goldfire

Upcoming partial type signatures and/or explicit type application will help, but these are both some distance away.

comment:4 Changed 5 years 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 5 years ago by simonpj

Cc: dimitris@… added


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?


comment:6 Changed 5 years 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 5 years 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


comment:8 Changed 5 years ago by Simon Peyton Jones <simonpj@…>

comment:9 Changed 5 years ago by Simon Peyton Jones <simonpj@…>

In 5770029a1f8509a673b2277287fc8fe90b9b6002/ghc:

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

comment:10 Changed 5 years ago by simonpj

Resolution: fixed
Status: newclosed
Test Case: indexed-types/should_compile/T9211
Note: See TracTickets for help on using tickets.