#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 goldfire): Perhaps this counterexample is why I could never finish that proof. I don't believe I ever reached for an assumption of finite types, probably conflating the notion of finite types with terminating type families. 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? Recall that infinite types have led to segfaults before: #8162. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11511#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler