
This might fall out of the implementation anyways, but a special case to be aware of is non-exhaustiveness in implicit kind variables, such the return kind of a polykinded type family, as arose in #11275: {{{ type family Hm :: k where Hm = Int }}} Despite appearances this type family is not exhaustive: `Hm :: (* -> *)` will not reduce. Yes, this makes a lot of sense, it really is non-exhaustive. If you think of
#10116: Closed type families: Warn if it doesn't handle all cases -------------------------------------+------------------------------------- Reporter: andrewthad | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.4 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 gkaracha): Replying to [comment:7 rwbarton]: the full type, I think that `Hm` would look like the following: {{{ type family Hm (k :: BOX) where Hm * = Int }}} Hence, we can compute the uncovered set to be: {{{ U1 = { k |> not (k ~ *) } }}} I think this is the only *clean* way to treat this, pretty close to what already happens with GADTs: Have both kind and type arguments explicit (kinds first) and represent the non-matched cases with kind inequalities. I suspect that proper kind inequalities (See [http://research.microsoft.com/en-us/um/people/simonpj/papers/ext-f /axioms-extended.pdf]) will be needed in order for the results of the check to be properly used by the type checker but I think that just for the warning it can be done in a simpler way. Can't be sure though! -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10116#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler