[GHC] #16059: checkValidType is defeated by a type synonym

[GHC]

#16059: checkValidType is defeated by a type synonym
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:  8.8.1
       Component:  Compiler (Type    |              Version:  8.7
  checker)                           |
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  GHC accepts       |  Unknown/Multiple
  invalid program                    |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by simonpj):

 `T14515` and friends.  I think it's reasonable to reject.  Type synonyms
 are not proper abstractions; they are more like macros.  The current
 behaviour:
 * Triggers unexpected new errors when you switch on `LiberalTypeSynonyms`.
 * Ditto if you manually expand a synonym, which should be innocuous.

 ----------------

 '''Timeouts'''. Look at `tc238`.  I thought at first that we were simply
 making an exponentially large type, as we easily could do:
 {{{
 type T1 = Int -> Int   -- Size = N
 type T2 = T1 -> T1     -- Size = 2N
 type T3 = T2 -> T2     -- Size = 4N
 ..
 }}}
   For such programs, I think it'd be fine to time out; we'd time out when
 ''using'' such a large synonym anyway.

   But that is NOT what is happening here.  For `tc238` we have
 {{{
 data T i r c = K (c i) (r c)

 type TIACons2  t x = T t (T t x)
 type TIACons3  t x = TIACons2 t (TIACons1 t x)
 type TIACons4  t x = TIACons2 t (TIACons2 t x)
 type TIACons7  t x = TIACons4 t (TIACons3 t x)
 type TIACons8  t x = TIACons4 t (TIACons4 t x)
 }}}
 So `TIACons2` has two occurrences of `T`; `TIACons3` has three, `TIACons4`
 has four; and so on.  The number in the name indicates the number of
 occurrences of T.  Big but not exponential.

 The problem comes because at each synonym we check validity with and
 without expansion. So if we have
 {{{
 type S = ...
 f :: S (S (S (S (S (S ....(S Int)...))))
 }}}
 we'll typecheck the outer S application with and without expansion; and in
 ''each'' of those checks we'll check the next S application with and
 without... result exponential!  This goes right back to Trac #323, 14
 years ago.

 What to do?  In general, we can't check both with and without expansion.
 So we could do one of these:

 1. Always expand.  That is simple and sound, but I suppose that it might
 occasionally yield a worse error message.

 2.  Always expand; but if you get an error message, then try without
 expansion to see if you also get an error; in the latter case report the
 latter error message not the former.

 3. Within the validity checker have a 3-way flag: Expand, NoExpand, Both.
 For Liberal start with Expand; for non-Liberal start with Both.

   Now at a synonym, in the Both case, switch to NoExpand when checking the
 non-expanded version, and to Both when checking the expanded version.

 I think (1) seems like a simpler starting point.

 ------------
 I agree about `synIsTau`.

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