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

 Replying to [comment:2 simonpj]:
 > So I suppose we should always validity-check the expansion, tiresome
 though that is.
 >
 > Would you like to do that?

 I tried this, and while this fixes this particular program, it introduces
 a myriad of test failures elsewhere:

 {{{
 Unexpected results from:
 TEST="Dep05 T13035 T14515 T9858a syn-perf2 tc160 tc238"
 }}}

 These can be categorized into the following categories:

 * Unexpected failures (`T14515`, `tc160`, `T9858a`)

   This is tricky. Consider the following minimized example:

   {{{#!hs
   {-# LANGUAGE RankNTypes #-}
   module A where

   type Foo = forall a. a -> a
   }}}
   {{{#!hs
   module B where

   import A

   foo :: Foo -> a -> a
   foo f x = f x
   }}}

   Currently, GHC HEAD accepts `B`. If we apply your suggested change,
 however, it is rejected:

   {{{
   $ ~/Software/ghc/inplace/bin/ghc-stage2 B.hs
   [1 of 2] Compiling A                ( A.hs, A.o )
   [2 of 2] Compiling B                ( B.hs, B.o )

   B.hs:5:8: error:
       • Illegal polymorphic type: forall a1. a1 -> a1
         Perhaps you intended to use RankNTypes or Rank2Types
       • In the expansion of type synonym ‘Foo’
         In the type signature: foo :: Foo -> a -> a
     |
   5 | foo :: Foo -> a -> a
     |        ^^^^^^^^^^^^^
   }}}

   Is this desirable? FWIW, GHC 8.6 also rejects `B`—it's only the current
 GHC HEAD that accepts it.
 * Timeouts (`T13035`, `tc238`, `syn-perf2`)

   It appears that having to fully expand every type synonym for validity-
 checking purposes imposes quite a bit of runtime cost.
 * Error message wibbles (`Dep05`)

   This happens simply because the more aggressive validity checking
 happens earlier now:

   {{{#!diff
   diff -uw "safeHaskell/unsafeLibs/Dep05.run/Dep05.stderr.normalised"
 "safeHaskell/unsafeLibs/Dep05.run/Dep05.comp.stderr.normalised"
   --- safeHaskell/unsafeLibs/Dep05.run/Dep05.stderr.normalised
 2018-12-17 08:54:30.765476910 -0500
   +++ safeHaskell/unsafeLibs/Dep05.run/Dep05.comp.stderr.normalised
 2018-12-17 08:54:30.765476910 -0500
   @@ -1,3 +1,23 @@

   -Dep05.hs:5:1:
   -    GHC.Arr: Can't be safely imported! The module itself isn't safe.
   +Dep05.hs:9:1:
   +     Illegal unboxed tuple type as function argument:
   +      (# GHC.Prim.State# s, a #)
   +      Perhaps you intended to use UnboxedTuples
   +     In the expansion of type synonym ‘GHC.ST.STRep’
   +      When checking the inferred type
   +        bad2 :: forall s e a.
   +                GHC.Prim.MutableArray# s e
   +                -> (Int, e) -> GHC.ST.STRep s a -> GHC.ST.STRep s a
   +
   +Dep05.hs:11:1:
   +     Illegal unboxed tuple type as function argument:
   +      (# GHC.Prim.State# s, Array i e #)
   +      Perhaps you intended to use UnboxedTuples
   +     In the expansion of type synonym ‘GHC.ST.STRep’
   +      When checking the inferred type
   +        bad3 :: forall i s e.
   +                i
   +                -> i
   +                -> Int
   +                -> GHC.Prim.MutableArray# s e
   +                -> GHC.ST.STRep s (Array i e)
   }}}

   This isn't too big of a deal, since we can suppress the new error
 message by enabling `UnboxedTuples`.

 > The `synIsTau` field of a `SynonymTyCon` might allow us to short-circuit
 the common case where the RHS is totally vanilla.  (To do so we'd need to
 ensure that `synIsTau` is false if there is a `=>` in the RHS, not just a
 forall.)

 That would work for this particular example, although there will likely be
 //other// validity checks that can't take advantage of this `synIsTau`
 shortcut. In fact, the original place I discovered this bug was in the
 context of a WIP patch I have which adds visible dependent quantification
 (i.e., [https://github.com/ghc-proposals/ghc-
 proposals/blob/36070b13d3f0970cda1faebc76afc220483340d6/proposals/0035
 -forall-arrow.rst this GHC proposal]). I discovered that GHC rejects this
 (since we can't yet have visible dependent quantification in the type of a
 term):

 {{{#!hs
 f :: forall k -> k -> Bool
 f = undefined
 }}}

 But //does// accept this:

 {{{#!hs
 type Foo = forall k -> k -> Bool

 f :: Foo
 f = undefined
 }}}

 The reason this happens is for the same reason as the original program in
 this ticket, so it would be nice if we could come up with a fix that
 covers both programs.

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