[GHC] #11514: Impredicativity is still sneaking in

[GHC]

#11514: Impredicativity is still sneaking in
-------------------------------------+-------------------------------------
        Reporter:  goldfire          |                Owner:  goldfire
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  8.1
      Resolution:                    |             Keywords:
                                     |  ImpredicativeTypes
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 RyanGlScott):

 Indeed, this //is// simply missing a check:

 {{{#!diff
 diff --git a/compiler/typecheck/TcUnify.hs b/compiler/typecheck/TcUnify.hs
 index 2ed861c..9280042 100644
 --- a/compiler/typecheck/TcUnify.hs
 +++ b/compiler/typecheck/TcUnify.hs
 @@ -2165,7 +2165,7 @@ metaTyVarUpdateOK dflags tv ty

  preCheck :: DynFlags -> Bool -> TcTyVar -> TcType -> OccCheckResult ()
  -- A quick check for
 ---   (a) a forall type (unless -XImpredivativeTypes)
 +--   (a) a forall type (unless -XImpredicativeTypes)
  --   (b) a type family
  --   (c) an occurrence of the type variable (occurs check)
  --
 @@ -2192,7 +2192,10 @@ preCheck dflags ty_fam_ok tv ty
        | bad_tc tc              = OC_Bad
        | otherwise              = mapM fast_check tys >> ok
      fast_check (LitTy {})      = ok
 -    fast_check (FunTy a r)     = fast_check a   >> fast_check r
 +    fast_check (FunTy a r)
 +      | not impredicative_ok
 +        && isPredTy a          = OC_Bad
 +      | otherwise              = fast_check a   >> fast_check r
      fast_check (AppTy fun arg) = fast_check fun >> fast_check arg
      fast_check (CastTy ty co)  = fast_check ty  >> fast_check_co co
      fast_check (CoercionTy co) = fast_check_co co
 }}}

 With that, the original program is rejected.

 There's one hiccup though: once this patch is applied, the `print027` test
 case begins to panic. Here is a minimized example of what happens:

 {{{
 $ inplace/bin/ghc-stage2 --interactive
 GHCi, version 8.7.20180729: http://www.haskell.org/ghc/  :? for help
 Loaded GHCi configuration from /home/rgscott/.ghci
 λ> :print (+)
 ghc-stage2: panic! (the 'impossible' happened)
   (GHC version 8.7.20180729 for x86_64-unknown-linux):
         isUnliftedType
   t1_a1Cn[rt] :: TYPE t_a1Cm[rt]
   Call stack:
       CallStack (from HasCallStack):
         callStackDoc, called at compiler/utils/Outputable.hs:1164:37 in
 ghc:Outputable
         pprPanic, called at compiler/types/Type.hs:2015:10 in ghc:Type
 }}}

 As far as I can tell, `:print` attempts to unify a unification variable
 `t1` with `Num a => a -> a -> a`, which fails. But `:print` proceeds
 onward anyways with the (not-unified) type `t1`, and falls over when it
 passes `t1` to `isUnliftedType`, which doesn't expect a type variable.

 This is worrying, but then again, `:print` has been known to trigger this
 `isUnliftedType` panic in other ways for some time now (see #14828). In
 light of this, I'm not sure if it's worth investing the effort to fix this
 `:print` panic, or just accept this as a known regression.

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