[GHC] #10116: Closed type families: Warn if it doesn't handle all cases

[GHC]

#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 goldfire):

 Replying to [comment:6 gkaracha]:
 >
 > So, my biggest concern is not the lack of linearity.

 Yes. Your argument above is convincing.

 > 1. Kind polymorphism is non-parametric and we can also have non-linear
 kind patterns

 I see how this can be troublesome. For example

 {{{
 data Proxy (a :: k) = P
 type family F (a :: k) where
   F 'P = Bool
 }}}

 elaborates to

 {{{
 type family F k (a :: k) where
   F (Proxy k a) ('P k a) = Bool
 }}}

 That last bit surely looks non-linear and incomplete, but it's actually OK
 because the type-system forces the `k`s and the `a`s to be the same.

 I actually think I have the solution to this, but it's a rather large
 change (actually originally motivated by other problems): invent a new
 type `TyPat` that stores type patterns (instance LHSs), something like
 this:

 {{{
 data TyPat
   = TyVarPat      TyVar
   | AppTyPat      TyPat TyPat
   | TyConTyPat    TyCon [TyPat]
   | DataConTyPat  DataCon [TyPat]
   | LitTyPat      TyLit
   | CoercionTyPat CoVar
 }}}

 This is quite like `Type`, but with a few notable changes:
 1. Though you can't see it above, the `[TyPat]` argument to `DataConTyPat`
 includes only ''existentials'', not universals. It is the universal
 arguments that are redundant in the polykinded case, and so skipping the
 universals means that the problem George brings up here goes away. It also
 solves an unrelated problem about type family applications appearing in
 universals -- these are harmless but are currently rejected because there
 should be no type family applications in type patterns.

 2. Casts are just missing, as they make no sense in patterns.

 3. Coercions (which will be datacon arguments always) are just bare
 coercion variables, as structurally matching coercions is bogus.

 4. There are no polytypes, as these never appear in patterns.

 These patterns would be used for type family LHSs and also class instance
 heads. I conjecture that the pure unifier (in the `Unify` module) could be
 written to take a `TyPat` and a `Type` instead of two `Type`s.

 Note that there isn't really a notion of a pattern's kind, due to the
 missing universals and casts. But I think that's OK. (Type variables in
 type patterns still have kinds, of course.)

 Anyway, sorry for this longish digression, but I do think it solves the
 problem here nicely and is a general improvement I wish to make.

 >
 > 2. Haskell is not lazy at the type level so I expect us to miss
 completeness which we can have at the term level due to laziness.

 Can you give an example? I don't understand.

 >
 > 3. I have no clue yet how to take injectivity annotations into account.

 Neither do I. But let's not let this stop us.

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