[GHC] #11424: "Occurs check" not considered when reducing closed type families

[GHC]

#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