Opened 4 years ago

Last modified 8 months ago

#11514 new bug

Impredicativity is still sneaking in

Reported by: goldfire Owned by: goldfire
Priority: normal Milestone:
Component: Compiler Version: 8.1
Keywords: ImpredicativeTypes Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

This is erroneously accepted:

{-# LANGUAGE RankNTypes #-}

module Bug where

foo :: forall a. (Show a => a -> a) -> ()
foo = undefined

undefined is being instantiated at (Show a => a -> a) -> (), which requires impredicativity. GHC does the right thing (reject!) if we try to instantiate with a type involving proper foralls.

I imagine this is a simple missing check.

Change History (4)

comment:1 Changed 3 years ago by simonpj

Keywords: ImpredicativeTypes added

comment:2 Changed 16 months ago by RyanGlScott

Indeed, this is simply missing a check:

  • compiler/typecheck/TcUnify.hs

    diff --git a/compiler/typecheck/TcUnify.hs b/compiler/typecheck/TcUnify.hs
    index 2ed861c..9280042 100644
    a b metaTyVarUpdateOK dflags tv ty 
    21652165
    21662166preCheck :: DynFlags -> Bool -> TcTyVar -> TcType -> OccCheckResult ()
    21672167-- A quick check for
    2168 --   (a) a forall type (unless -XImpredivativeTypes)
     2168--   (a) a forall type (unless -XImpredicativeTypes)
    21692169--   (b) a type family
    21702170--   (c) an occurrence of the type variable (occurs check)
    21712171--
    preCheck dflags ty_fam_ok tv ty 
    21922192      | bad_tc tc              = OC_Bad
    21932193      | otherwise              = mapM fast_check tys >> ok
    21942194    fast_check (LitTy {})      = ok
    2195     fast_check (FunTy a r)     = fast_check a   >> fast_check r
     2195    fast_check (FunTy a r)
     2196      | not impredicative_ok
     2197        && isPredTy a          = OC_Bad
     2198      | otherwise              = fast_check a   >> fast_check r
    21962199    fast_check (AppTy fun arg) = fast_check fun >> fast_check arg
    21972200    fast_check (CastTy ty co)  = fast_check ty  >> fast_check_co co
    21982201    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.

comment:3 Changed 16 months ago by simonpj

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.

Yes it looks exactly like #14828. I'd be inlined to accept the regression.

But it would be great if someone was to actually look at #14828.

comment:4 Changed 8 months ago by Marge Bot <ben+marge-bot@…>

In 8d18a873/ghc:

Reject nested predicates in impredicativity checking

When GHC attempts to unify a metavariable with a type containing
foralls, it will be rejected as an occurrence of impredicativity.
GHC was /not/ extending the same treatment to predicate types, such
as in the following (erroneous) example from #11514:

```haskell
foo :: forall a. (Show a => a -> a) -> ()
foo = undefined
```

This will attempt to instantiate `undefined` at
`(Show a => a -> a) -> ()`, which is impredicative. This patch
catches impredicativity arising from predicates in this fashion.

Since GHC is pickier about impredicative instantiations, some test
cases needed to be updated to be updated so as not to fall afoul of
the new validity check. (There were a surprising number of
impredicative uses of `undefined`!) Moreover, the `T14828` test case
now has slightly less informative types shown with `:print`. This is
due to a a much deeper issue with the GHCi debugger (see #14828).

Fixes #11514.
Note: See TracTickets for help on using tickets.