[GHC] #15954: LiberalTypeSynonyms unsaturation check doesn't kick in

[GHC]

#15954: LiberalTypeSynonyms unsaturation check doesn't kick in
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:  8.6.3
       Component:  Compiler (Type    |              Version:  8.6.2
  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 RyanGlScott):

 Thanks, I've implemented your suggestion. There are three error message
 regressions as a result, so I'd like your feedback on them.

 1. In `T15859`:

 {{{#!diff
 diff -uw "dependent/should_fail/T15859.run/T15859.stderr.normalised"
 "dependent/should_fail/T15859.run/T15859.comp.stderr.normalised"
 --- dependent/should_fail/T15859.run/T15859.stderr.normalised   2018-11-27
 06:38:24.627899584 -0500
 +++ dependent/should_fail/T15859.run/T15859.comp.stderr.normalised
 2018-11-27 06:38:24.635899818 -0500
 @@ -1,6 +1,7 @@

 -T15859.hs:13:5:
 -     Cannot apply expression of type ‘forall k -> k -> *’
 -      to a visible type argument ‘Int’
 +T15859.hs:13:19:
 +     Illegal polymorphic type: forall k -> k -> *
 +      Perhaps you intended to use LiberalTypeSynonyms
 +     In an expression type signature: KindOf A
 +      In the expression: undefined :: KindOf A
       In the expression: (undefined :: KindOf A) @Int
 -      In an equation for ‘a’: a = (undefined :: KindOf A) @Int
 }}}

    This one doesn't bother me much, since that code really ought to have
 been enabling `LiberalTypeSynonyms` in the first place (indeed,
 investigating that code is what led me to discovering this bug). I think
 I'll fix this by just enabling `LiberalTypeSynonyms` in the test case.

 2. In `T7809`:

 {{{#!diff
 diff -uw "typecheck/should_fail/T7809.run/T7809.stderr.normalised"
 "typecheck/should_fail/T7809.run/T7809.comp.stderr.normalised"
 --- typecheck/should_fail/T7809.run/T7809.stderr.normalised     2018-11-27
 06:42:45.604510107 -0500
 +++ typecheck/should_fail/T7809.run/T7809.comp.stderr.normalised
 2018-11-27 06:42:45.615510428 -0500
 @@ -1,6 +1,5 @@

  T7809.hs:8:8:
 -     Illegal polymorphic type: PolyId
 +     Illegal polymorphic type: forall a. a -> a
        GHC doesn't yet support impredicative polymorphism
 -     In the type signature:
 -        foo :: F PolyId
 +     In the type signature: foo :: F PolyId
 }}}

    This one is a bit concerning, since we've regressed from a nice error
 message about `PolyId` (which is what the user wrote) to instead
 mentioning `forall a. a -> a` (which requires the user to perform some
 detective work to figure out where it comes from). I haven't figured out
 yet why this happens (indeed, I'm surprised to see a type synonym being
 expanded //more// after this change).

 3. In `tc149`:

 {{{
 Compile failed (exit code 1) errors were:

 tc149.hs:8:8: error:
     • The type synonym ‘Id’ should have 1 argument, but has been given
 none
     • In the type signature: foo :: Generic Id Id
 }}}

    This is the most concerning one, since `tc149` is actually expected to
 //typecheck//! For the sake of reference, here is the source code for this
 test case:

 {{{#!hs
 {-# LANGUAGE RankNTypes #-}

 module ShouldCompile where

 type Generic i o = forall x. i x -> o x
 type Id x = x

 foo :: Generic Id Id
 foo = error "urk"

 -- The point here is that we instantiate "i" and "o"
 -- with a partially applied type synonym.  This is
 -- OK in GHC because we check type validity only *after*
 -- expanding type synonyms.
 --
 -- However, a bug in GHC 5.03-Feb02 made this break a
 -- type invariant (see Type.mkAppTy)
 }}}


    Mysteriously, that comment claims that this code ought to typecheck as-
 is. But shouldn't that only be the case if `LiberalTypeSynonyms` is
 enabled?

    This test case was added all the way back in 2002 (in commit
 ddb3ea2220621d9393ebb08ce3548ac2118a57c2) without much exposition, so it's
 difficult for me to tell whether this test case is legitimate or not.

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