GitLab

@rae reports the following issue, introduced by the removal of flattening variables (8bb52d91).

{-# LANGUAGE TypeFamilies, FunctionalDependencies, FlexibleInstances,
             FlexibleContexts, ScopedTypeVariables #-}

module Bug where

type family F a
class C a b | a -> b where
  meth :: a -> b -> ()

g :: forall a b. (F b ~ F a) => a -> b -> ()
g x y = const () (meth True x, meth False y, [undefined :: F a, True])

    * Reduction stack overflow; size = 201
      When simplifying the following type: F a
      Use -freduction-depth=0 to disable this check
      (any upper bound you could choose might fail unpredictably with
       minor updates to GHC, so disabling the check is recommended if
       you're sure that type checking should terminate)
    * In the expression: undefined :: F a
      In the expression: [undefined :: F a, True]
      In the second argument of `const', namely
        `(meth True x, meth False y, [undefined :: F a, True])'
   |
11 | g x y = const () (meth True x, meth False y, [undefined :: F a, True])
   |                                               ^^^^^^^^^^^^^^^^

The problem is that we end up with inerts:

[G] co {0} :: F b[sk:1] ~# F a[sk:1] (CEqCan)
[D] _ {0}:: a[sk:1] ~# b[sk:1] (CEqCan)

and work item

[D] _ {0}:: F a[sk:1] ~# Bool (CEqCan)

This causes a loop as the substitution associated to the inert set is not terminating, rewriting F a to F b (using the Derived) then back to F a (using the Given).

---

Note that a similar situation can happen if we allow Wanteds to rewrite Wanteds (see test case T3440):

 type family Fam a :: Type

 data GADT :: Type -> Type where
   GADT :: a -> Fam a -> GADT (Fam a)

 unwrap :: GADT (Fam a) -> (a, Fam a)
 unwrap (GADT x y) = (x, y)

In that case we end up with inert set

[G] F b[sk:1] ~# F a[sk:1] (CEqCan)
[W] a[sk:1] ~# b[sk:1] (CEqCan)

which causes the same loop when trying to rewrite another wanted involving a or b.