#11514: Impredicativity is still sneaking in -------------------------------------+------------------------------------- Reporter: goldfire | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.1 Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- 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. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11514> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#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: | -------------------------------------+------------------------------------- Changes (by simonpj): * keywords: => ImpredicativeTypes -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11514#comment:1> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#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
#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 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. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11514#comment:3> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#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 Marge Bot <ben+marge-bot@…>): In [changeset:"8d18a873c5d7688c6e7d91efab6bb0d6f99393c6/ghc" 8d18a873/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="8d18a873c5d7688c6e7d91efab6bb0d6f99393c6" 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. }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11514#comment:4> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
participants (1)
-
GHC