#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): Ah, you bring up a good point. I suppose the thing we really should be scrutinizng is `Cast a b Refl x = x`. I'm also a bit baffled that that doesn't work either—after all, something quite similar works at the term level! {{{#!hs {-# LANGUAGE GADTs #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeOperators #-} import Data.Type.Equality cast :: a :~: b -> a -> b -> Int cast Refl (_ :: a) (_ :: b) = 42 }}} I'm aware that this is a bit of a strawman, since comparing type families and scoped type pattern variables is a bit apples-and-oranges. But surely you can see the point I'm driving at here—if `a` and `b` are equated by the pattern match on `Refl`, should we reject the use of two syntactically different type variables for the second and third arguments of `cast`? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14366#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler