[GHC] #12950: unnecessarily complicated left-hand side causing RULE left-hand side too complicated to desugar

[GHC]

#12950: unnecessarily complicated left-hand side causing RULE left-hand side too
complicated to desugar
-------------------------------------+-------------------------------------
        Reporter:  nfrisby           |                Owner:
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  7.10.2
  checker)                           |
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  Incorrect         |  Unknown/Multiple
  error/warning at compile-time      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:  #10555,#12074     |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by nfrisby):

 I'm unfamiliar with the implementation of the type-checker. Even so, I
 flipped on `-ddump-tc-trace` to investigate where that troublesome
 coercion was coming from. I noticed the following subsequence of trace
 messages.

 {{{
 tcSubTypeDS_NC
   the type signature for ‘overloaded’
   a_awb[tau:1] -> (a_awb[tau:1], TF a_awb[tau:1])
   Int -> (Int, TF Int)
 *snip*
 writeMetaTyVar a_awb[tau:1] := Int
 *snip*
 utype_defer
   cobox_awd
   TF a_awb[tau:1]
   TF Int
   arising from a type equality a_awb[tau:1]
                                -> (a_awb[tau:1], TF a_awb[tau:1])
                                ~
                                Int -> (Int, TF Int)
 *snip*
 u_tys yields coercion: cobox_awd
 }}}

 This indicates that `cobox_awd` is the result of the unifier deferring the
 question of whether `TF a_awb ~ TF Int`, even though `a_awd` was already
 set to `Int`.

 Digging a bit deeper, I see that `TcUnify.uType` contains
 [https://github.com/ghc/ghc/blob/086b4836c4b279d5ae0e330719e1a679dd16392e/compiler/typecheck/TcUnify.hs#L1286-L1291
 the following matches], which ultimately incur the coercion that sinks the
 SPECIALISE pragma since they do not check if the types' already solved
 tyvars admit reflexivity as a proof here.

 {{{#!hs
         -- Always defer if a type synonym family (type function)
         -- is involved.  (Data families behave rigidly.)
     go ty1@(TyConApp tc1 _) ty2
       | isTypeFamilyTyCon tc1 = uType_defer origin ty1 ty2
     go ty1 ty2@(TyConApp tc2 _)
       | isTypeFamilyTyCon tc2 = uType_defer origin ty1 ty2
 }}}

 I anticipate that a possible "fix" for this ticket would be for the `go`
 function to check if the solved type variables render `ty1` and `ty2`
 equivalent such that `TcRefl` would suffice here. Or perhaps there's
 somewhere more appropriate (`dsSpec`?) to perform that "optimization" for
 the sake of accepting SPECIALIZE pragmas like this one.

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