#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