#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): I don't think that a direct "substitution" lemma makes sense in this context---remember that `F a` may not refer to a type at all, so we can't just put it in a place where a type is expected. So, if we had some type-expression `t`, and wanted to substitute `F a` for some variable `b`, we wouldn't do a direct substitution, but rather, we'd emit a new constraint: `F a ~ b`. Basically, the idea is that type functions are not really first class types, but may "introduce" types via constraints like: `F a ~ b`. So, if I write a type like `Maybe (F a)`, what I really mean is `(F a ~ b) => Maybe b`. Of course, if we can prove that `F a` is always defined we may "short-cut" the constraint part and just treat it as an ordinary type, but that's optional. This is basically the same idea is the "functional notation for functional dependencies" (section 3 of "Language and Program Design for Functional Dependencies"). -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11424#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler