[GHC] #10327: Devise workaround for how infinite types prevent closed type family reduction

[GHC]

#10327: Devise workaround for how infinite types prevent closed type family
reduction
-------------------------------------+-------------------------------------
              Reporter:  goldfire    |             Owner:
                  Type:  feature     |            Status:  new
  request                            |         Milestone:
              Priority:  normal      |           Version:  7.10.1
             Component:  Compiler    |  Operating System:  Unknown/Multiple
              Keywords:              |   Type of failure:  None/Unknown
          Architecture:              |        Blocked By:
  Unknown/Multiple                   |   Related Tickets:
             Test Case:              |
              Blocking:              |
Differential Revisions:              |
-------------------------------------+-------------------------------------
 Suppose we have

 {{{
 data a :+: b

 type family Inj x y where
   Inj a a = True
   Inj b (b :+: c) = False
 }}}

 When we try to reduce `Inj f (f :+: g)`, it looks like we should just use
 the second equation. Instead, we fail to reduce. This is because GHC is
 worried about the possibility of the first equation firing, in the event
 that `f ~ (f :+: g)`. This fact can happen only if `f` is infinitely
 large. On the surface, this seems impossible, but shenanigans in this area
 can cause `unsafeCoerce`. See #8162.

 I don't see an easy way to fix this, but the fact that GHC can't cope
 (well) with this example tells me something is wrong. Here is one idea of
 how to proceed:

 If we somehow ensure at reduction time that `f` is finite, we're OK. If we
 need finiteness in terms, we use `deepseq`. Can we do this in types? I
 tentatively say "yes".

 Imagine the following type family:

 {{{
 type family Seq (x :: a) (y :: b) :: b

 type instance Seq True  y = y
 type instance Seq False y = y
 }}}

 To reduce, say, {{{b `Seq` 5}}}, we'd need to know concretely what `b` is.
 We can then build `Deepseq` similarly to how `deepseq` at the term level
 works.

 The closed type family mechanism could then detect cases like `Inj`, where
 the whole infinite-type thing is causing trouble. (I conjecture that
 detecting this is not hard, as there's a specific line in the `Unify`
 module that triggers in the worry-about-infinite-types case.) In the case
 of `Inj`, something like `Inj f (f :+: g)` would reduce to {{{f `Deepseq`
 False}}}. Note that the call to `Seq` wouldn't be written in the closed
 type family definition, but would be inserted during reduction as
 appropriate.

 This solution is ugly. And it requires magic to define `Seq` in types (we
 need an instance for every type!) and weird magic in closed type family
 reduction. The definition of `Deepseq` might also benefit from being
 magical. It would be annoying to explain to users, but no more so than the
 current crazy story. In general, I don't like this idea much, but I do
 think it would work.

 In any case, this ticket is mainly to serve as a placeholder for any
 future thoughts in this direction. It's quite annoying to have the specter
 of infinite types cripple otherwise-sensible closed type families.

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