#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