[GHC] #14366: Type family equation refuses to unify wildcard type patterns

[GHC]

#14366: Type family equation refuses to unify wildcard type patterns
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  8.2.1
  checker)                           |             Keywords:  TypeFamilies,
      Resolution:                    |  TypeInType
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:                    |
-------------------------------------+-------------------------------------

Comment (by RyanGlScott):

 After reading #14938, I now understand at least //why// this is happening.
 I was operating under the misconception that pattern-matching in type
 families brings a coercion into scope, which would "force" the two
 wildcards in `Cast _ _ Refl x = x` to unify. But this isn't the case at
 all, as https://ghc.haskell.org/trac/ghc/ticket/14938#comment:5
 explains—matching on `Refl` //requires// a coercion  in order to type-
 check.

 Unfortunately, the way type wildcards work is at odds with this, because
 early on in the renamer, GHC simply renames `Cast _ _ Refl x = x` to
 something like `Cast _1 _2 Refl x = x`. Because `_1` and `_2` aren't the
 same, matching on `Refl :: _1 :~: _1` isn't going to work.

 It seems like we'd need to somehow defer the gensymming of wildcard names
 until during typechecking to make this work. But the details of that are
 beyond me.

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