[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 gkaracha):

 Replying to [comment:9 goldfire]:
 > 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)

 I really like this, having a separate data type for type patterns would
 certainly be a nice
 change and make things a lot easier.

 > > 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.
 Hmmm, I have the following in mind:
 {{{#!hs
 data G = MkG G

 -- term level
 f :: G -> G
 f x = x -- non-redundant (inhabited by _|_, MkG _|_, etc)

 -- type level
 type family F (a :: G) :: G where
   F x = x -- redundant?
 }}}

 The way I see it, we can never construct a type of kind `G`, in contrast
 to the term level
 where every type is inhabited by bottom. Hence, at the term level, the
 checker does not need
 to unfold `x` to `MkG (MkG (...))`, for checking whether the clause is
 redundant. At the type
 level, I would expect the check to try this, and of course diverge. Does
 this make sense?

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