#11424: "Occurs check" not considered when reducing closed type families -------------------------------------+------------------------------------- Reporter: diatchki | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.1 checker) | Resolution: | Keywords: 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 diatchki): Perhaps there is a different way to do the reduction that avoids this problem. My mental model of type functions is that: 1. they only ever ***name*** types, they never introduce ***new*** types, which arise from `data`, `newtype` and primitives. 2. they may be partial, so sometimes they don't name any type at all. I find it easiest to think about all this in terms of GHC's internal representation of the constraints, so your example would look something like this: {{{ (Same a [a] ~ Char, Loop Int ~ a) }}} Now, I think reducing `Same a [a] ~ Char` to `Char ~ Char`, and then just eliminating it as a trivial equality is perfectly valid. However, eliminating the `Loop Int ~ a` constraint is what's questionable here, even if `a` is not used anywhere. This constraint essentially says that `Loop Int` must be well-defined, in other words, it better refer to an actual ground type that exists. One (fairly simple?) way for GHC to check the validity of such constraints would be to simply evaluate them until it does find the ground type in question. In your example, this would result in GHC non-terminating during type checking, which is perfectly reasonable, especially since you need `UndecidableInstaces` to write such recursive types. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11424#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler