Opened 5 years ago
Last modified 17 months ago
#10116 new feature request
Closed type families: Warn if it doesn't handle all cases
Reported by: | andrewthad | Owned by: | |
---|---|---|---|
Priority: | normal | Milestone: | |
Component: | Compiler | Version: | 7.8.4 |
Keywords: | TypeFamilies, PatternMatchWarnings | Cc: | jstolarek, george.karachalias@…, tom.schrijvers@…, RyanGlScott |
Operating System: | Unknown/Multiple | Architecture: | Unknown/Multiple |
Type of failure: | Incorrect warning at compile-time | Test Case: | |
Blocked By: | Blocking: | ||
Related Tickets: | Differential Rev(s): | ||
Wiki Page: |
Description (last modified by )
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.
Change History (17)
comment:1 Changed 5 years ago by
Cc: | jan.stolarek@… added |
---|---|
Description: | modified (diff) |
Type: | task → feature request |
comment:2 Changed 5 years ago by
Cc: | george.karachalias@… tom.schrijvers@… added |
---|
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
comment:3 follow-up: 6 Changed 5 years ago by
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.
comment:4 Changed 4 years ago by
Cc: | jstolarek added; jan.stolarek@… removed |
---|
comment:5 Changed 4 years ago by
Cc: | RyanGlScott added |
---|
comment:6 follow-up: 9 Changed 4 years ago by
Replying to 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 (http://people.cs.kuleuven.be/~george.karachalias/papers/p424-karachalias.pdf) to make the clauses semi-linear (linear but interleaved with guards - every non-linear pattern matching can be transformed this way), the match becomes:
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:
- Kind polymorphism is non-parametric and we can also have non-linear kind patterns
- 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.
- 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.
comment:7 follow-up: 8 Changed 4 years ago by
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.
comment:8 Changed 4 years ago by
Replying to 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 = IntDespite 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
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!
comment:9 follow-up: 10 Changed 4 years ago by
Replying to gkaracha:
So, my biggest concern is not the lack of linearity.
Yes. Your argument above is convincing.
- 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:
- Though you can't see it above, the
[TyPat]
argument toDataConTyPat
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.
- Casts are just missing, as they make no sense in patterns.
- Coercions (which will be datacon arguments always) are just bare coercion variables, as structurally matching coercions is bogus.
- 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.
- 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.
- I have no clue yet how to take injectivity annotations into account.
Neither do I. But let's not let this stop us.
comment:10 Changed 4 years ago by
Replying to 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.
- 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:
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?
comment:11 follow-up: 12 Changed 4 years ago by
G
is inhabited at the type level, by Any
for example. And by
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.
comment:12 Changed 4 years ago by
Replying to goldfire:
G
is inhabited at the type level, byAny
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. :-)
comment:13 follow-up: 14 Changed 4 years ago by
Any
needs UndecidableInstances
? I don't think it should...
comment:14 Changed 4 years ago by
Replying to goldfire:
Any
needsUndecidableInstances
? I don't think it should...
Oops, sorry, my mistake, Any
does not need UndecidableInstances
!
I had a different implementation of Any
in mind.
comment:15 Changed 4 years ago by
Type of failure: | None/Unknown → Incorrect warning at compile-time |
---|
comment:16 Changed 4 years ago by
Keywords: | TypeFamilies added |
---|
comment:17 Changed 17 months ago by
Keywords: | PatternMatchWarnings added |
---|
Checking pattern exhaustiveness for closed type families could also allow us to detect unreachable equations:
Here the last equation is unreachable but GHC does not discover this.