[GHC] #11511: Type family producing infinite type accepted as injective

[GHC]

#11511: Type family producing infinite type accepted as injective
-------------------------------------+-------------------------------------
        Reporter:  jstolarek         |                Owner:
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  8.1
  checker)                           |             Keywords:  TypeFamilies,
      Resolution:                    |  Injective
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by adamgundry):

 > What bothers me is that we have no guarantee that FC types are indeed
 finite. On paper, we just define types inductively and are done with it.
 But how does this play out in the implementation?

 I suppose it might be possible to accidentally define an "infinite" type
 or coercion as a lazy value, but surely Core Lint would go into a loop
 when checking it? What other problems do you envisage?

 > Recall that infinite types have led to segfaults before: #8162.

 That's a slightly different issue: the type family overlap check was
 unsound because it treated `a` and `a -> a` as apart, even though `a ~ a
 -> a` is solvable in the presence of non-terminating type families.
 Crucially, it is possible to construct a ''finite'' proof of `a ~ a -> a`
 that contradicts the overlap check. Whereas in this case, the only
 "proofs" of `F Bool ~ F Char` are infinite (and hence non-constructible).

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