[GHC] #12175: Instance resolution regression

[GHC]

#12175: Instance resolution regression
-------------------------------------+-------------------------------------
           Reporter:  crockeea       |             Owner:
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.0.1
           Keywords:                 |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  GHC rejects
  Unknown/Multiple                   |  valid program
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 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

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12175>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler