#16278: Exhaustivity checking GADT with free variables -------------------------------------+------------------------------------- Reporter: andrewthad | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.3 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 andrewthad): Thanks for the insights! I’m not certain that GHC replaces the polymorphic type variable with Any before the exhaustiveness check happens. (Although I suspect it does). If it does, then is unfortunate that we end up doing an apartness check for `'Send` an `Any` when what should actually happen is an apartness check for `'Send` and `forall (s :: Send). s` (talking about the second example where I omitted the type annotation). You make a good argument that teaching the compiler about apartness involving type families in the general case is difficult or maybe in possible. But there are more specific cases where deciding apartness is a more tractable problem. You could consider only non-recursive type families, only type families that don’t mention other type families, nullary type families, or the combination of all three (aka Any). From what I’ve found in the GHC wiki, it looks like the apartness check is an approximation anyway. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16278#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler