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

 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