[GHC] #10116: Closed type families: Warn if it doesn't handle all cases
#10116: Closed type families: Warn if it doesn't handle all cases -------------------------------------+------------------------------------- Reporter: andrewthad | Owner: Type: task | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.4 Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Blocked By: Test Case: | Related Tickets: Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Right now, I can do the following: data Foo = A | B type family Bar (n :: 'Foo) where Bar 'A = Int I would like to be warned if I write a partial type function like this because partial functions are almost always a mistake. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10116 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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: Type of failure: None/Unknown | Unknown/Multiple Blocked By: | Test Case: Related Tickets: | Blocking: | Differential Revisions: -------------------------------------+------------------------------------- Changes (by jstolarek): * cc: jan.stolarek@… (added) * type: task => feature request Old description:
Right now, I can do the following:
data Foo = A | B type family Bar (n :: 'Foo) where Bar 'A = Int
I would like to be warned if I write a partial type function like this because partial functions are almost always a mistake.
New description: Right now, I can do the following: {{{#!hs data Foo = A | B type family Bar (n :: 'Foo) where Bar 'A = Int }}} I would like to be warned if I write a partial type function like this because partial functions are almost always a mistake. -- Comment: Checking pattern exhaustiveness for closed type families could also allow us to detect unreachable equations: {{{#!hs data Foo = A | B type family Bar (n :: Foo) where Bar 'A = Int Bar 'B = Char Bar a = Double }}} Here the last equation is unreachable but GHC does not discover this. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10116#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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: Type of failure: None/Unknown | Unknown/Multiple Blocked By: | Test Case: Related Tickets: | Blocking: | Differential Revisions: -------------------------------------+------------------------------------- Changes (by simonpj): * cc: george.karachalias@…, tom.schrijvers@… (added) Comment: George Karachalias and Tom Schrijvers are busy building a cool new pattern-match checker for GHC. We have an ICFP submission nearly finished; I'll put it up in a day or three. Once it's in, it could probably be adapted to do type families too, but it'd be a bit of work. Simon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10116#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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: Type of failure: None/Unknown | Unknown/Multiple Blocked By: | Test Case: Related Tickets: | Blocking: | Differential Revisions: -------------------------------------+------------------------------------- Comment (by 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. For example: {{{ type family F (a :: Bool) (b :: Maybe Bool) :: Nat where F True (Just False) = 0 F False (Just True) = 1 F x (Just x) = 2 F y Nothing = 3 }}} Is that total? I do believe it is. But it's a little hard to figure it out! But we could certainly do ''something'' in this area. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10116#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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 Revisions: -------------------------------------+------------------------------------- Changes (by jstolarek): * cc: jan.stolarek@… (removed) * cc: jstolarek (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10116#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * cc: RyanGlScott (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10116#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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
#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 rwbarton): 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10116#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
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
#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
#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
#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): `G` is inhabited at the type level, by `Any` for example. And by {{{#!hs type family Loopy :: G where Loopy = MkG Loopy }}} Normally, using something like `Loopy` in a program will cause GHC to issue an error, but sufficient cleverness can get this past the type- checker. So I would say your `F`'s equation is not redundant at all. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10116#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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:11 goldfire]:
`G` is inhabited at the type level, by `Any` for example.
Oh, I see, right, Yet, both `Any` and `Loopy` need `UndecidableInstances`. Is there a way to inhabit `G` without enabling `UndecidableInstances`? I expect a good check to be able to handle everything anyway, I am just asking in an attempt to identify a subset of the language for which the check can have nice properties. :-) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10116#comment:12 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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): `Any` needs `UndecidableInstances`? I don't think it should... -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10116#comment:13 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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:13 goldfire]:
`Any` needs `UndecidableInstances`? I don't think it should...
Oops, sorry, my mistake, `Any` does not need `UndecidableInstances`! I had a different implementation of `Any` in mind. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10116#comment:14 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10116: Closed type families: Warn if it doesn't handle all cases -------------------------------------+------------------------------------- Reporter: andrewthad | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.4 Resolution: | Keywords: TypeFamilies, | PatternMatchWarnings Operating System: Unknown/Multiple | Architecture: Type of failure: Incorrect | Unknown/Multiple warning at compile-time | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * keywords: TypeFamilies => TypeFamilies, PatternMatchWarnings -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10116#comment:17 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC