#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