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 jstolarek)

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 jstolarek

Cc: jan.stolarek@… added
Description: modified (diff)
Type: taskfeature request

Checking pattern exhaustiveness for closed type families could also allow us to detect unreachable equations:

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.

comment:2 Changed 5 years ago by simonpj

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 Changed 5 years ago 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.

comment:4 Changed 4 years ago by jstolarek

Cc: jstolarek added; jan.stolarek@… removed

comment:5 Changed 4 years ago by RyanGlScott

Cc: RyanGlScott added

comment:6 in reply to:  3 ; Changed 4 years ago by gkaracha

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:

  1. Kind polymorphism is non-parametric and we can also have non-linear kind patterns
  1. 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.
  1. 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.

Last edited 4 years ago by gkaracha (previous) (diff)

comment:7 Changed 4 years ago 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.

comment:8 in reply to:  7 Changed 4 years ago by gkaracha

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 = 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 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 in reply to:  6 ; Changed 4 years ago by goldfire

Replying to 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 ks and the as 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.
  1. Casts are just missing, as they make no sense in patterns.
  1. Coercions (which will be datacon arguments always) are just bare coercion variables, as structurally matching coercions is bogus.
  1. 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 Types.

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.

  1. 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.

  1. 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 in reply to:  9 Changed 4 years ago by gkaracha

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.

  1. 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 Changed 4 years ago by goldfire

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 in reply to:  11 Changed 4 years ago by gkaracha

Replying to 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. :-)

comment:13 Changed 4 years ago by goldfire

Any needs UndecidableInstances? I don't think it should...

comment:14 in reply to:  13 Changed 4 years ago by gkaracha

Replying to 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.

comment:15 Changed 4 years ago by thomie

Type of failure: None/UnknownIncorrect warning at compile-time

comment:16 Changed 4 years ago by thomie

Keywords: TypeFamilies added

comment:17 Changed 17 months ago by simonpj

Keywords: PatternMatchWarnings added
Note: See TracTickets for help on using tickets.