#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