Spurious untouchable type variable in connection with rank-2 type and constraint family

The following code cannot be compiled:

{-# LANGUAGE ConstraintKinds, Rank2Types, TypeFamilies #-}

import GHC.Exts (Constraint)

type family F a b :: Constraint

data T b c = T

f :: (forall b . F a b => T b c) -> a
f _ = undefined

GHC outputs the following error message:

Untouchable.hs:9:6: error:
    • Couldn't match type ‘c0’ with ‘c’
        ‘c0’ is untouchable
          inside the constraints: F a b
          bound by the type signature for:
                     f :: F a b => T b c0
          at Untouchable.hs:9:6-37
      ‘c’ is a rigid type variable bound by
        the type signature for:
          f :: forall a c. (forall b. F a b => T b c) -> a
        at Untouchable.hs:9:6
      Expected type: T b c0
        Actual type: T b c
    • In the ambiguity check for ‘f’
      To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
      In the type signature:
        f :: (forall b. F a b => T b c) -> a

Trac metadata

Trac field	Value
Version	8.2.1-rc2
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler (Type checker)
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture

changed weight to 5

added Tbug Trac import typechecker labels

I can see that it seems odd. Imagine that you wrote

f :: (forall b . F a b => T b c) -> a
f _ = undefined

g :: (forall bb . F aa bb => T bb cc) -> aa
g x = f x

You'd expect that to work: the two signatures are the same. But in the call in g's rhs we have:

Expected type of f's arg:              forall b. F a0 b => T b c0)
Actual type of x (after instantation): T bb0 cc
           plus a "wanted" constraint: F aa bb0

where the "0" things are unification variables. Of course this is easily soluble by unifying bb0=b, a0=aa, c0=cc. The a0=aa is enforced by the result type of the call to (f x) but the other two are not. And the "untouchable" bit is because we don't unify under a given equality constraint, or something that might be a given equality, like (F a0 b). (Why: see the OutsideIn paper.)

The ambiguity check, which is failing here, is precisely implementing this reasoning.

In short: it's all behaving as designed. The error message is unhelpful, but it IS a subtle issue.

I wish I could be more helpful.

added Pnormal label

Is this another instance of #9223 (closed) or a separate bug? I'm also experiencing something very similar to this (and working around it by passing a Proxy to c).

This bug is really about generating a good error message (as was #9223 (closed)). I do think it can be improved, so I'm leaving this open, but it's not likely to be addressed any time soon.

@trac-yairchu, would you be able to post your example here?

@rae sure, my example is in the definition traverseKWith_ here -

https://github.com/lamdu/syntax-tree/blob/master/src/AST/Class/Combinators.hs#L147

For some context, I'm trying to make a variation of Functor and friends where the items are indexed, and furthermore their indexes are also indexed recursively (tying the knot via a newtype Knot = Knot (Knot -> Type)).

This allows me to express indexed AST types, such as the one in your Stitch paper (which is indexed on scopes), while using an external fix-point. This allows us for example to describe the diff of two terms just by using the Diff knot as a fixpoint.

traverseKWith_, which exhibits the bug, is the KFoldable version of traverse_, but unlike traverseK_ (without a "with"), the "with" stands for working with a list of type classes which the indexes for the contained items have instances for.

Because of this bug, it has to use foldMapKWith' (with ') rather than foldMapKWith. The difference is an extra Proxy argument to work around this type error.

I just tried to build your project on GHC 8.6, but my build dies with

src/AST/Internal/TH.hs:69:9: error:
    • Couldn't match expected type ‘TyVarBndr’ with actual type ‘Type’
    • In the pattern: SigT (VarT var) (ConT knot)
      In a case alternative:
          SigT (VarT var) (ConT knot) | knot == ''Knot -> pure (res, var)
      In the expression:
        case last xs of
          SigT (VarT var) (ConT knot) | knot == ''Knot -> pure (res, var)
          VarT var -> pure (res, var)
          _ -> fail "expected last argument to be a knot variable"
   |
69 |         SigT (VarT var) (ConT knot) | knot == ''Knot -> pure (res, var)
   |         ^^^^^^^^^^^^^^^^^^^^^^^^^^^

Do I need a different version of something?

@rae, try building with --constraint='th-abstraction<0.3', as the breaking changes in th-abstraction-0.3.* are likely the culprit. (Doing so made it work for me.)

@RyanGlScott indeed! I now checked and also got an error using a newer th-abstraction version. Added the constraint to the .cabal file now. Thanks!

OK. I've gotten it to compile. But everything seems to be behaving as expected. We really can't infer the types here, because ApplyKConstraints might introduce an equality constraint. And I think GHC is correct in not being sure what type you want. I grant that the error message is a bit rough-going, but so is this code (as in, it uses a lot of type-level features).

It is worth saying that you don't need a proxy. Instead, you could write foldMapKWith @[f ()], using -XTypeApplications. I've tested this and it works nicely.

Is there a better error message you seek?

First, thanks for the TypeApplications suggestion! I'll use that and avoid the work-around combinators!

As for what I seek -

I understand that the ApplyKConstraints constraints child inside foldMapKWith's type might introduce equality constraints, but don't we know that these constraints can't possibly include a? Because a is a forall that's not related to neither constraints nor child via any functional dependency or anything, so can't we at least convince ourselves that we can safely unify it with [f ()]?? Am I missing something?

We have

foldMapKWith ::
    (Monoid a, KFoldable k, KLiftConstraints constraints (ChildrenTypesOf k)) =>
    Proxy constraints ->
    (forall child. ApplyKConstraints constraints child => Tree n child -> a) ->
    Tree k n -> a

When we are examining foldMapKWith p ((:[]) . f), We process ((:[]) . f) with expected type forall child. ApplyKConstraints constraints child => Tree n child -> a. But actually, we're trying to infer constraints, n, and a there. So really the expected type is forall child. ApplyKConstraints constraints0 child => Tree n0 child -> a0, where I've marked unification variables with 0.

Your point is that, no matter what ApplyKConstraints constraints0 child is, a0 is untouched. I agree, but that doesn't solve our problem. Suppose we determine that ((:[]) . f) results in [Int]. What should a0 be? If ApplyKConstraints constraints0 child includes the equality constraints0 ~ [Int], then maybe a0 and constraints0 are the same. Or maybe a0 is just [Int]. We don't know. And therein lies the problem: we need to know this to be able to infer the type.

mentioned in issue #17105 (closed)

See also #17105 (closed) for another example.

I ran into this problem when defining a data type to hold a value m x that could be used in the monads that satisfy mc. I intend to use this in a library that mocks values for testing.

data HoldsMonad (mc :: (Type -> Type) -> Constraint)
  = forall x . Typeable x => HoldsMonad (forall m . mc m => m x)

holdsIntInMonadIO :: HoldsMonad MonadIO
holdsIntInMonadIO = HoldsMonad (pure 1 :: forall m . MonadIO m => m Int)

It fails to compile with

    • Could not deduce (Typeable x0)
         omitting this error for brevity - it is caused by the error below
    • Couldn't match type ‘x0’ with ‘x’
        ‘x0’ is untouchable
          inside the constraints: mc m
          bound by a type expected by the context:
                     forall (m :: * -> *). mc m => m x0
          at <interactive>:84:56-115
      ‘x’ is a rigid type variable bound by
        the type of the constructor ‘HoldsMonad’:
          forall (mc :: (* -> *) -> Constraint) x.
          Typeable x =>
          (forall (m :: * -> *). mc m => m x) -> HoldsMonad mc
        at <interactive>:84:56-115
      Expected type: m x0
        Actual type: m x
    • In the ambiguity check for ‘HoldsMonad’
      To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
      In the definition of data constructor ‘HoldsMonad’
      In the data type declaration for ‘HoldsMonad’

It is not clear if TypeApplications can help here since the error happens at the definition site. Is there a way to rewrite the data type to achieve the same result?

I agree that you've found another example of this ticket. As with the other cases here, the error is genuine: for an abstract mc -- which could imply an equality constraint -- we really can't be sure that x is unambiguous.

The solution for this case is easy, though: just enable -XAllowAmbiguousTypes. That will accept the original definition, and I believe concrete usages (like HoldsMonad MonadIO will not need -XAllowAmbiguousTypes to be on.

In all the cases in this ticket, I claim rejection is correct -- it's just that the error message is hard to figure out.