[GHC] #13705: Failure of improvement for type-family dependencies

[GHC]

#13705: Failure of improvement for type-family dependencies
-------------------------------------+-------------------------------------
        Reporter:  simonpj           |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  8.0.1
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by simonpj):

 This program shows up a bug in the pure unifier in `Unify.hs`.  Look at
 {{{
 unify_ty ty1 (TyVarTy tv2) kco
   = do { unif <- amIUnifying
        ; if unif
          then umSwapRn $ uVar tv2 ty1 (mkSymCo kco)
          else surelyApart }  -- non-tv on left; tv on right: can't match.
 }}}
 If we are matching
 {{{
    F a ~ b
 }}}
 where `F` is a type function, we want to ''succeed'', not return
 `SurelyApart`, because in Algorithm U/M from the paper, type function
 applications are treated like wildcards.  And indeed a later equation
 deals with that case
 {{{
 unify_ty ty1 _ _
   | Just (tc1, _) <- splitTyConApp_maybe ty1
   , not (isGenerativeTyCon tc1 Nominal)
   = maybeApart
 }}}
 It's just that the type-variable case was too eager.

 Easy to fix.

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