[GHC] #11581: TypeError requires UndecidableInstances unnecessarily

[GHC]

#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