#11581: TypeError requires UndecidableInstances unnecessarily -------------------------------------+------------------------------------- Reporter: rwbarton | Owner: Type: feature request | Status: new Priority: low | Milestone: Component: Compiler (Type | Version: 8.0.1-rc2 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by rwbarton): Replying to [comment:2 simonpj]:
For `TypeError` we know for sure since it is built in. For now we could make it a special case: easy to do and useful.
Yes, that's one option. I was in a bit of a rush when writing the ticket so let me try to explain what I meant by the last paragraph. I think the undecidability checker is computing the size of the type family application wrong. Compare these type family declarations: {{{#!hs type family T1 (a :: *) (b :: *) :: * type family T2 (a :: *) :: * -> * }}} and suppose I use one of these in the right-hand side of another type family: {{{#!hs type instance F Int a b = T1 String (a,b) -- or: T2 String (a,b) }}} If I used `T1`, the compiler definitely needs to take into account the size of both arguments because `T1` can match on both arguments. But if I used `T2`, then `T2` can only match on its first argument, and so `T2 String` is a saturated type family application, which has been further applied to `(a,b)`. This latter application is generative (if `f x ~ T2 String (a,b)` then `f ~ T2 String` and `x ~ (a,b)`) and so it is just as "inert" from the standpoint of type family reduction as if I had written {{{#!hs data Ap (f :: * -> *) a type instance F Int a b = Ap (T2 String) (a,b) }}} which the undecidability checker happily accepts. In short, I think the undecidability checker should only include the indexed arguments to a type family when calculating the size of a type family application, and not any additional parametric arguments. But it doesn't work that way currently. That's why I tried writing `type family TypeError :: ErrorMessage -> b where` rather than the current definition `type family TypeError (a :: ErrorMessage) :: b where`. In the case of `TypeError`, there is an additional twist: `TypeError` has an implicit kind argument. I couldn't figure out how to tell GHC that `TypeError` is parametric in the kind argument too, at least judging from the `:i TypeError` output. Shouldn't that be possible? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11581#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler