#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