[GHC] #11594: closed empty type families fully applied get reduced lazily when in a constraint tuple and fully applied

[GHC]

#11594: closed empty type families  fully applied get reduced lazily when in a
constraint tuple and fully applied
-------------------------------------+-------------------------------------
        Reporter:  carter            |                Owner:
            Type:  feature request   |               Status:  new
        Priority:  normal            |            Milestone:  8.0.1
       Component:  Compiler (Type    |              Version:  7.10.2
  checker)                           |
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:  #9636             |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by adamgundry):

 Replying to [comment:6 carter]:
 > So if I wanted a new userland insolvable type family that errors out
 eagerly rather than down stream, I'd have to have a type solver plugin
 active in the defining module to enforce that?
 >
 > I guess that would enable simulating the type error family in userland
 In 7.10 right?

 The plugin would need to be active at use sites, not definition sites, but
 yes - it is possible for plugins to approximately simulate `TypeError`.
 They can't give exactly the same semantics, because plugins only get to
 see unsolved constraints, but can work the same way for uses of
 `TypeError` at kind `Constraint`.

 In fact I hacked together a quick prototype plugin that does exactly that
 during the last ICFP. If there's interest, I'm happy to share the code,
 though it's not entirely consistent with the `TypeError` API.


 > What if instead, when defining an empty closed type family, we could
 pragma
 > Annotate it with "requires plugin foo" when we want this other plugin
 adhuncated semantics,
 > Because otherwise requiring the offending type plugin is implicit in any
 down stream module!

 Right, there is currently no way to indicate which type-checker plugins a
 module requires, and it might be nice to do so.

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11594#comment:8>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler