[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:                    |
-------------------------------------+-------------------------------------
Changes (by adamgundry):

 * cc: adamgundry (added)


Comment:

 I don't think this is a soundness problem: FC does not have infinite
 types, only finite approximations thereof, and there is no way to prove
 the equality of any finite expansions of `F Bool` and `F Char`.

 Here's a hand-wavy argument that injectivity of `F` is admissible...
 Suppose we have a minimal coercion `F s ~ F t`. Then either this is by
 congruence of type family application (in which case we have `s ~ t`), or
 it uses the axiom for `F` to expand both sides, so there is a smaller
 coercion `[F s] ~ [F t]` and hence of `F s ~ F t` (which contradicts the
 assumption that our original coercion was minimal). [The ordering on
 coercions is left as an exercise to the reader.]

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