#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

#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: | Unknown/Multiple Type of failure: GHC rejects | Test Case: indexed- valid program | types/should_compile/T11581 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * testcase: => indexed-types/should_compile/T11581 Comment:

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.

Good point. And easily actioned. Thanks. That still leaves the `TypeError` special case, which I have not done anything about yet. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11581#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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: | Unknown/Multiple Type of failure: GHC rejects | Test Case: indexed- valid program | types/should_compile/T11581 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * cc: goldfire (added) Comment: I dunno. Maybe these days you can say {{{ type family TypeError :: forall k (b::k). ErrorMessage b }}} We'll have to ask Richard, our kind-polymorphism king. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11581#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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: | Unknown/Multiple Type of failure: GHC rejects | Test Case: indexed- valid program | types/should_compile/T11581 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by rwbarton): Empty and closed. Exactly like it is now except having arity 0 rather than 2 (as it does currently) or 1 (best I can seem to do currently). -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11581#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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: | Unknown/Multiple Type of failure: GHC rejects | Test Case: indexed- valid program | types/should_compile/T11581 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by rwbarton): What exactly is the plan, though? This doesn't work even after a008eadf: {{{#!hs {-# LANGUAGE TypeFamilies, TypeInType, RankNTypes #-} module Arity where import GHC.Types import GHC.TypeLits hiding (TypeError) type family TypeError :: forall b. ErrorMessage -> b where {} type family T (a :: Type) :: Type where T t = TypeError (ShowType t) }}} {{{ rwbarton@morphism:/tmp$ ~/ghc-newest/inplace/bin/ghc-stage2 -fprint- explicit-kinds Arity.hs [1 of 1] Compiling Arity ( Arity.hs, Arity.o ) Arity.hs:10:3: error: • The type family application ‘TypeError Type’ is no smaller than the instance head (Use UndecidableInstances to permit this) • In the equations for closed type family ‘T’ In the type family declaration for ‘T’ }}} So I hope the plan involves changing the calculation of the arity of a type family to not include kind arguments that only appear in the result kind of the type family, or something like that. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11581#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler