[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 goldfire):

 Replying to [comment:2 diatchki]:
 > 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.
 >

 Except that means that type families can't work over abstract types that
 we don't know much about yet. For example:

 {{{
 type family Equals a b where
   Equals a a = True
   Equals a b = False
 }}}

 I `Equals x x` to reduce to `True` even if I don't know what `x` is. Under
 your scheme, I would need to know what `x` is to be able to make progress,
 if only to ensure that it terminates.

 This whole thing is a sad story. But I don't know how to make it better.
 See also #10327 and [https://typesandkinds.wordpress.com/2015/09/09/what-
 are-type-families/ my blog post] on the subject
 ([https://www.reddit.com/r/haskell/comments/3kyfrl/richard_eisenberg_what_are_type_families/
 reddit comments on blog post]). Bottom line: I think the Right Solution is
 to require all non-associated type families to be total (implying
 terminating) and force all non-total type families to be associated with a
 class constraint. (This actually makes them functional dependencies in
 disguise!) Then these problems go away.

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11424#comment:3>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler