#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