Instance resolution regression

The following code works in 7.10, but fails in GHC 8.0.1:

{-# LANGUAGE ConstraintKinds, MultiParamTypeClasses, TypeFamilies,
             UndecidableInstances #-}

import GHC.Exts

class Foo a
instance (Foo a, Foo b, CTypeOf a ~ CTypeOf b) => Foo (a,b)

type family TElt r :: Constraint
type instance TElt r = (Foo r, Dispatch (CTypeOf r) r)

type family CTypeOf x where CTypeOf (a,b) = CTypeOf a

class (repr ~ CTypeOf r) => Dispatch repr r

data CT r = CT [r]

toCT :: (Foo r) => CT r -> CT r
toCT = undefined

unzipT :: (TElt a, TElt b, TElt (a,b)) => CT (a,b) -> (CT a, CT b)
unzipT = unzipT . toCT

main :: IO ()
main = undefined

with the errors

Main.hs:1:1: error:
    solveWanteds: too many iterations (limit = 4)
      Unsolved: WC {wc_simple =
                      [D] _ :: Dispatch fsk_a3GC b (CDictCan)
                      [W] hole{a3Hh} :: CTypeOf a ~ CTypeOf b (CNonCanonical)
                      [D] _ :: fsk_a3GC ~ CTypeOf b (CDictCan)
                      [D] _ :: fsk_a3GC ~ CTypeOf b (CDictCan)
                      [D] _ :: fsk_a3GC ~ CTypeOf b (CNonCanonical)}
      New superclasses found
      Set limit with -fconstraint-solver-iterations=n; n=0 for no limit

Main.hs:22:19: error:
    • Couldn't match type ‘CTypeOf a’ with ‘CTypeOf b’
        arising from a use of ‘toCT’
      NB: ‘CTypeOf’ is a type function, and may not be injective
    • In the second argument of ‘(.)’, namely ‘toCT’
      In the expression: unzipT . toCT
      In an equation for ‘unzipT’: unzipT = unzipT . toCT
    • Relevant bindings include
        unzipT :: CT (a, b) -> (CT a, CT b) (bound at Main.hs:22:1)

I don't understand the first error at all. The second error seems to be due to calling toCT on the type CT (a,b), which requires the constraint Foo (a,b). Rather than using the supplied constraint from TElt (a,b), GHC is trying to resolve the instance provided, which requires CType a ~ CType b.

Possibly related: #10338, #11948 (closed)

Trac metadata

Trac field	Value
Version	8.0.1
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture