#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