[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:3 goldfire]:
 > I conjecture that getting this completely right for closed type families
 is a research project of its own, because closed type families allow for
 repeated variables.

 Hmmmm, I agree that it is a research project on its own but I have been
 working
 on it the past months. If we use the technique we use in the [PAPER] to
 make
 the clauses semi-linear (linear but interleaved with guards - every non-
 linear
 pattern matching can be transformed this way), the match becomes:

 {{{#!hs
 type family F (a :: Bool) (b :: Maybe Bool) :: Nat where
   F True  (Just False)     = 0
   F False (Just True)      = 1
   F x     (Just z (z ~ x)) = 2
   F y     Nothing          = 3
 }}}

 Hence, by applying the algorithm as is we get (I omit constraints Delta
 where
 we don't have any or where they are just variable bindings that do not
 refer
 to the same variable):

 {{{
 U1 = { False x1, True Nothing, True (Just True) }

 U2 = { False Nothing, False (Just False)
      , True Nothing
      , True (Just True) }

 U3 = { False Nothing
      , False (Just False) |> {x ~ False, z ~ False, not (z ~ x)}   --
 inconsistent
      , True Nothing
      , True  (Just True)  |> {x ~ True,  z ~ True,  not (z ~ x)} } --
 inconsistent

 -- and cleaned up
 U3 = { False Nothing, True  Nothing }

 U4 = {}
 }}}

 So, my biggest concern is not the lack of linearity. I also seem to have
 found
 a way to treat explicit type applications in patterns. The issues that
 still
 bother me a bit are the following:

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

 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.

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

 I have plenty of ideas for 1 and 2 (at least on paper they seem to work)
 but I
 expect the 3rd to be more challenging to address.  I am not setting myself
 as
 the owner yet, unless I find a way to incorporate the above but I hope to
 do so
 in 2016. :)

 George

 P.S. And since closed type families are usually MUCH smaller than term
 level
 functions and also they do not allow arbitrary guards (yet at least) but
 only
 the ones the check will generate, I expect such a check to be performant,
 in
 contrast to term-level pattern match checking.

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