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

26 Nov 2018

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

 {{{#!hs
 {-# LANGUAGE ImpredicativeTypes #-}
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE RankNTypes #-}
 module Bug where

 import GHC.Exts (Any)

 type KindOf (a :: k) = k
 type A a = (Any :: a)
 type KA = KindOf A
 }}}

 But it really oughtn't to. After all, we have an unsaturated use of `A` in
 `KindOf A`, and we don't have `LiberalTypeSynonyms` enabled!

 What's even stranger is that there seems to be something about this exact
 setup that sneaks by `LiberalTypeSynonyms`' validity checks. If I add
 another argument to `A`:

 {{{#!hs
 type A x a = (Any :: a)
 }}}

 Then it //does// error:

 {{{
 $ /opt/ghc/8.6.2/bin/ghc Bug.hs
 [1 of 1] Compiling Bug              ( Bug.hs, Bug.o )

 Bug.hs:10:1: error:
     • Illegal polymorphic type: forall a -> a
       Perhaps you intended to use LiberalTypeSynonyms
     • In the type synonym declaration for ‘KA’
    |
 10 | type KA = KindOf A
    | ^^^^^^^^^^^^^^^^^^
 }}}

 Similarly, if I use something besides `KindOf`:

 {{{#!hs
 {-# LANGUAGE ImpredicativeTypes #-}
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE RankNTypes #-}
 module Bug where

 import GHC.Exts (Any)

 type A a = (Any :: a)
 type B a = Int
 type C = B A
 }}}

 Then I also get the same `Illegal polymorphic type: forall a -> a` error.

-- 
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15954
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler