So at the points when a (closed) type family expression has to be evaluated, e.g., for equality comparison, and it cannot be reduced then
#9636: Function with type error accepted -------------------------------------+------------------------------------- Reporter: augustss | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.3 Resolution: | Keywords: Operating System: | Architecture: Unknown/Multiple Unknown/Multiple | Difficulty: Unknown Type of failure: | Blocked By: None/Unknown | Related Tickets: Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (by goldfire): Replying to [comment:16 augustss]: this should be an error. IMHO. Unfortunately, this, too, violates the substitution lemma. We probably want to be able to solve `(a ~ a)` with reflexivity, for ''any'' `a`. But, you're suggesting that a particular value for `a`, namely `T Bool`, will ''not'' equal itself. The difference between types and terms here is that we need to be able to reason about unevaluated types, such as `a`. We never need this ability on terms, so the existing term-level semantics works out just fine. To be clear, I'm saying that issuing an error/warning in the case of a user-written strange beast seems quite easy to implement. Any suggestion beyond that made here seems like a stretch, though. Do keep suggesting, though -- perhaps we'll find something that works in here. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9636#comment:17 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler