Reject nested predicates in impredicativity checking
authorRyan Scott <ryan.gl.scott@gmail.com>
Sun, 17 Mar 2019 13:37:27 +0000 (09:37 -0400)
committerMarge Bot <ben+marge-bot@smart-cactus.org>
Thu, 21 Mar 2019 00:10:57 +0000 (20:10 -0400)
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.

20 files changed:
compiler/typecheck/TcErrors.hs
compiler/typecheck/TcUnify.hs
testsuite/tests/dependent/should_compile/dynamic-paper.hs
testsuite/tests/dependent/should_compile/dynamic-paper.stderr
testsuite/tests/ghci.debugger/scripts/print027.stdout
testsuite/tests/ghci/scripts/T12447.script
testsuite/tests/ghci/scripts/T14828.stdout
testsuite/tests/indexed-types/should_compile/T4358.hs
testsuite/tests/indexed-types/should_fail/T5934.stderr
testsuite/tests/polykinds/T11142.stderr
testsuite/tests/polykinds/T14270.hs
testsuite/tests/polykinds/T9569.hs
testsuite/tests/th/T11452.stderr
testsuite/tests/typecheck/should_compile/T12427a.stderr
testsuite/tests/typecheck/should_fail/T10194.stderr
testsuite/tests/typecheck/should_fail/T11514.hs [new file with mode: 0644]
testsuite/tests/typecheck/should_fail/T11514.stderr [new file with mode: 0644]
testsuite/tests/typecheck/should_fail/T12563.stderr
testsuite/tests/typecheck/should_fail/T12589.stderr
testsuite/tests/typecheck/should_fail/all.T

index 1d639d7..6cbe61b 100644 (file)
@@ -16,7 +16,7 @@ import GhcPrelude
 import TcRnTypes
 import TcRnMonad
 import TcMType
-import TcUnify( occCheckForErrors, OccCheckResult(..) )
+import TcUnify( occCheckForErrors, MetaTyVarUpdateResult(..) )
 import TcEnv( tcInitTidyEnv )
 import TcType
 import RnUnbound ( unknownNameSuggestions )
@@ -1632,7 +1632,7 @@ mkTyVarEqErr' dflags ctxt report ct oriented tv1 co1 ty2
         , report
         ]
 
-  | OC_Occurs <- occ_check_expand
+  | MTVU_Occurs <- occ_check_expand
     -- We report an "occurs check" even for  a ~ F t a, where F is a type
     -- function; it's not insoluble (because in principle F could reduce)
     -- but we have certainly been unable to solve it
@@ -1657,10 +1657,10 @@ mkTyVarEqErr' dflags ctxt report ct oriented tv1 co1 ty2
        ; mkErrorMsgFromCt ctxt ct $
          mconcat [important main_msg, extra2, extra3, report] }
 
-  | OC_Bad <- occ_check_expand
+  | MTVU_Bad <- occ_check_expand
   = do { let msg = vcat [ text "Cannot instantiate unification variable"
                           <+> quotes (ppr tv1)
-                        , hang (text "with a" <+> what <+> text "involving foralls:") 2 (ppr ty2)
+                        , hang (text "with a" <+> what <+> text "involving polytypes:") 2 (ppr ty2)
                         , nest 2 (text "GHC doesn't yet support impredicative polymorphism") ]
        -- Unlike the other reports, this discards the old 'report_important'
        -- instead of augmenting it.  This is because the details are not likely
index d8b1edf..cbf98d8 100644 (file)
@@ -31,7 +31,7 @@ module TcUnify (
   matchActualFunTys, matchActualFunTysPart,
   matchExpectedFunKind,
 
-  metaTyVarUpdateOK, occCheckForErrors, OccCheckResult(..)
+  metaTyVarUpdateOK, occCheckForErrors, MetaTyVarUpdateResult(..)
 
   ) where
 
@@ -2115,43 +2115,43 @@ with (forall k. k->*)
 
 -}
 
-data OccCheckResult a
-  = OC_OK a
-  | OC_Bad     -- Forall or type family
-  | OC_Occurs
+data MetaTyVarUpdateResult a
+  = MTVU_OK a
+  | MTVU_Bad     -- Forall, predicate, or type family
+  | MTVU_Occurs
 
-instance Functor OccCheckResult where
+instance Functor MetaTyVarUpdateResult where
       fmap = liftM
 
-instance Applicative OccCheckResult where
-      pure = OC_OK
+instance Applicative MetaTyVarUpdateResult where
+      pure = MTVU_OK
       (<*>) = ap
 
-instance Monad OccCheckResult where
-  OC_OK x    >>= k = k x
-  OC_Bad     >>= _ = OC_Bad
-  OC_Occurs  >>= _ = OC_Occurs
+instance Monad MetaTyVarUpdateResult where
+  MTVU_OK x    >>= k = k x
+  MTVU_Bad     >>= _ = MTVU_Bad
+  MTVU_Occurs  >>= _ = MTVU_Occurs
 
-occCheckForErrors :: DynFlags -> TcTyVar -> Type -> OccCheckResult ()
--- Just for error-message generation; so we return OccCheckResult
+occCheckForErrors :: DynFlags -> TcTyVar -> Type -> MetaTyVarUpdateResult ()
+-- Just for error-message generation; so we return MetaTyVarUpdateResult
 -- so the caller can report the right kind of error
 -- Check whether
 --   a) the given variable occurs in the given type.
 --   b) there is a forall in the type (unless we have -XImpredicativeTypes)
 occCheckForErrors dflags tv ty
   = case preCheck dflags True tv ty of
-      OC_OK _   -> OC_OK ()
-      OC_Bad    -> OC_Bad
-      OC_Occurs -> case occCheckExpand [tv] ty of
-                     Nothing -> OC_Occurs
-                     Just _  -> OC_OK ()
+      MTVU_OK _   -> MTVU_OK ()
+      MTVU_Bad    -> MTVU_Bad
+      MTVU_Occurs -> case occCheckExpand [tv] ty of
+                       Nothing -> MTVU_Occurs
+                       Just _  -> MTVU_OK ()
 
 ----------------
 metaTyVarUpdateOK :: DynFlags
                   -> TcTyVar             -- tv :: k1
                   -> TcType              -- ty :: k2
                   -> Maybe TcType        -- possibly-expanded ty
--- (metaTyFVarUpdateOK tv ty)
+-- (metaTyVarUpdateOK tv ty)
 -- We are about to update the meta-tyvar tv with ty
 -- Check (a) that tv doesn't occur in ty (occurs check)
 --       (b) that ty does not have any foralls
@@ -2178,17 +2178,18 @@ metaTyVarUpdateOK dflags tv ty
   = case preCheck dflags False tv ty of
          -- False <=> type families not ok
          -- See Note [Prevent unification with type families]
-      OC_OK _   -> Just ty
-      OC_Bad    -> Nothing  -- forall or type function
-      OC_Occurs -> occCheckExpand [tv] ty
+      MTVU_OK _   -> Just ty
+      MTVU_Bad    -> Nothing  -- forall, predicate, or type function
+      MTVU_Occurs -> occCheckExpand [tv] ty
 
-preCheck :: DynFlags -> Bool -> TcTyVar -> TcType -> OccCheckResult ()
+preCheck :: DynFlags -> Bool -> TcTyVar -> TcType -> MetaTyVarUpdateResult ()
 -- A quick check for
---   (a) a forall type (unless -XImpredivativeTypes)
---   (b) a type family
---   (c) an occurrence of the type variable (occurs check)
+--   (a) a forall type (unless -XImpredicativeTypes)
+--   (b) a predicate type (unless -XImpredicativeTypes)
+--   (c) a type family
+--   (d) an occurrence of the type variable (occurs check)
 --
--- For (a) and (b) we check only the top level of the type, NOT
+-- For (a), (b), and (c) we check only the top level of the type, NOT
 -- inside the kinds of variables it mentions.  But for (c) we do
 -- look in the kinds of course.
 
@@ -2198,25 +2199,28 @@ preCheck dflags ty_fam_ok tv ty
     details          = tcTyVarDetails tv
     impredicative_ok = canUnifyWithPolyType dflags details
 
-    ok :: OccCheckResult ()
-    ok = OC_OK ()
+    ok :: MetaTyVarUpdateResult ()
+    ok = MTVU_OK ()
 
-    fast_check :: TcType -> OccCheckResult ()
+    fast_check :: TcType -> MetaTyVarUpdateResult ()
     fast_check (TyVarTy tv')
-      | tv == tv' = OC_Occurs
+      | tv == tv' = MTVU_Occurs
       | otherwise = fast_check_occ (tyVarKind tv')
            -- See Note [Occurrence checking: look inside kinds]
 
     fast_check (TyConApp tc tys)
-      | bad_tc tc              = OC_Bad
+      | bad_tc tc              = MTVU_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{ft_af = af, ft_arg = a, ft_res = r})
+      | InvisArg <- af
+      , not impredicative_ok   = MTVU_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
     fast_check (ForAllTy (Bndr tv' _) ty)
-       | not impredicative_ok = OC_Bad
+       | not impredicative_ok = MTVU_Bad
        | tv == tv'            = ok
        | otherwise = do { fast_check_occ (tyVarKind tv')
                         ; fast_check_occ ty }
@@ -2226,13 +2230,13 @@ preCheck dflags ty_fam_ok tv ty
      -- For kinds, we only do an occurs check; we do not worry
      -- about type families or foralls
      -- See Note [Checking for foralls]
-    fast_check_occ k | tv `elemVarSet` tyCoVarsOfType k = OC_Occurs
+    fast_check_occ k | tv `elemVarSet` tyCoVarsOfType k = MTVU_Occurs
                      | otherwise                        = ok
 
      -- For coercions, we are only doing an occurs check here;
      -- no bother about impredicativity in coercions, as they're
      -- inferred
-    fast_check_co co | tv `elemVarSet` tyCoVarsOfCo co = OC_Occurs
+    fast_check_co co | tv `elemVarSet` tyCoVarsOfCo co = MTVU_Occurs
                      | otherwise                       = ok
 
     bad_tc :: TyCon -> Bool
index c998f09..1188bf1 100644 (file)
@@ -34,7 +34,7 @@ fromInteger = Prelude.fromInteger
 
 insertStore = undefined
 schema = undefined
-withTypeable = undefined
+withTypeable _ _ = undefined
 throw# = undefined
 
 toDynamicST = undefined
index a170d29..56da989 100644 (file)
@@ -12,4 +12,4 @@ Simplifier ticks exhausted
   simplifier non-termination has been judged acceptable.
    
   To see detailed counts use -ddump-simpl-stats
-  Total ticks: 140007
+  Total ticks: 140086
index 3117eac..eb5b363 100644 (file)
@@ -1,6 +1,6 @@
-+ = (_t1::Num a => a -> a -> a)
-print = (_t2::Show a1 => a1 -> IO ())
-log = (_t3::Floating a2 => a2 -> a2)
-head = (_t4::[a4] -> a4)
-tail = (_t5::[a7] -> [a7])
-fst = (_t6::(a11, b) -> a11)
++ = (_t1::t1)
+print = (_t2::t1)
+log = (_t3::t1)
+head = (_t4::[a] -> a)
+tail = (_t5::[a1] -> [a1])
+fst = (_t6::(a2, b) -> a2)
index 6003a43..3bdd3f4 100644 (file)
@@ -4,6 +4,6 @@ import Data.Typeable
 
 class Deferrable p where deferEither :: proxy p -> (p => r) -> Either String r
 
-instance (Typeable a, Typeable b) => Deferrable (a ~ b) where deferEither = undefined
+instance (Typeable a, Typeable b) => Deferrable (a ~ b) where deferEither _ _ = undefined
 
 :t deferEither @(_ ~ _)
index 3ef2e60..9ccea0c 100644 (file)
@@ -6,7 +6,7 @@ return :: Monad m => a -> m a
 return = (_t3::t1)
 pure :: Applicative f => a -> f a
 pure = (_t4::t1)
-mempty = (_t5::Monoid a => a)
-mappend = (_t6::Monoid a => a -> a -> a)
+mempty = (_t5::t1)
+mappend = (_t6::t1)
 foldl' = (_t7::t1)
 f = (_t8::t1)
index 0c05576..cb05a1c 100644 (file)
@@ -6,6 +6,6 @@ type family T a
 
 t2 :: forall a. ((T a ~ a) => a) -> a
 t2 = t
-  
+
 t :: forall a. ((T a ~ a) => a) -> a
-t = undefined
+t = undefined
index 21af0d8..e7448a9 100644 (file)
@@ -1,7 +1,7 @@
 
 T5934.hs:12:7: error:
     • Cannot instantiate unification variable ‘a0’
-      with a type involving foralls: (forall s. GenST s) -> Int
+      with a type involving polytypes: (forall s. GenST s) -> Int
         GHC doesn't yet support impredicative polymorphism
     • In the expression: 0
       In an equation for ‘run’: run = 0
index a3b40c1..4f5c5fc 100644 (file)
@@ -7,7 +7,7 @@ T11142.hs:9:49: error:
 
 T11142.hs:10:7: error:
     • Cannot instantiate unification variable ‘a0’
-      with a type involving foralls:
+      with a type involving polytypes:
         (forall k1 (a :: k1). SameKind a b) -> ()
         GHC doesn't yet support impredicative polymorphism
     • In the expression: undefined
index 3eed83c..d578be3 100644 (file)
@@ -76,7 +76,7 @@ splitApp rep@(TrFun _ a b) = Just (IsApp (mkTrApp arr a) b)
 splitApp (TrTyCon{})       = Nothing
 
 withTypeable :: forall a r. TypeRep a -> (Typeable a => r) -> r
-withTypeable = undefined
+withTypeable _ _ = undefined
 
 eqTypeRep :: forall k1 k2 (a :: k1) (b :: k2).
              TypeRep a -> TypeRep b -> Maybe (a :~~: b)
index 1b8bb68..634d742 100644 (file)
@@ -11,7 +11,7 @@ class Deferrable (c :: Constraint) where
 
 deferPair :: (Deferrable c1, Deferrable c2) =>
                   Proxy (c1,c2) -> ((c1,c2) => a) -> a
-deferPair = undefined
+deferPair _ _ = undefined
 
 instance (Deferrable c1, Deferrable c2) => Deferrable (c1,c2) where
     -- defer p f = deferPair p f     -- Succeeds
index 32064a9..e4f1cc6 100644 (file)
@@ -8,7 +8,7 @@ T11452.hs:6:14: error:
 
 T11452.hs:6:14: error:
     • Cannot instantiate unification variable ‘p0’
-      with a type involving foralls: forall a. a -> a
+      with a type involving polytypes: forall a. a -> a
         GHC doesn't yet support impredicative polymorphism
     • In the Template Haskell quotation [|| \ _ -> () ||]
       In the expression: [|| \ _ -> () ||]
index 05e9260..efc87a1 100644 (file)
@@ -3,7 +3,8 @@ T12427a.hs:17:29: error:
     • Couldn't match expected type ‘p’
                   with actual type ‘(forall b. [b] -> [b]) -> Int’
       ‘p’ is a rigid type variable bound by
-        the inferred type of h11 :: T -> p at T12427a.hs:17:1-29
+        the inferred type of h11 :: T -> p
+        at T12427a.hs:17:1-29
     • In the expression: v
       In a case alternative: T1 _ v -> v
       In the expression: case y of { T1 _ v -> v }
@@ -12,7 +13,7 @@ T12427a.hs:17:29: error:
 
 T12427a.hs:28:6: error:
     • Cannot instantiate unification variable ‘p0’
-      with a type involving foralls: (forall b. [b] -> [b]) -> Int
+      with a type involving polytypes: (forall b. [b] -> [b]) -> Int
         GHC doesn't yet support impredicative polymorphism
     • In the pattern: T1 _ x1
       In a pattern binding: T1 _ x1 = undefined
index 7bc79b2..aeaad79 100644 (file)
@@ -1,7 +1,7 @@
 
 T10194.hs:7:8: error:
-    Cannot instantiate unification variable ‘b0’
-    with a type involving foralls: X
-      GHC doesn't yet support impredicative polymorphism
-    In the expression: (.)
-    In an equation for ‘comp’: comp = (.)
+    • Cannot instantiate unification variable ‘b0’
+      with a type involving polytypes: X
+        GHC doesn't yet support impredicative polymorphism
+    • In the expression: (.)
+      In an equation for ‘comp’: comp = (.)
diff --git a/testsuite/tests/typecheck/should_fail/T11514.hs b/testsuite/tests/typecheck/should_fail/T11514.hs
new file mode 100644 (file)
index 0000000..f0dc07a
--- /dev/null
@@ -0,0 +1,6 @@
+{-# LANGUAGE RankNTypes #-}
+
+module T11514 where
+
+foo :: forall a. (Show a => a -> a) -> ()
+foo = undefined
diff --git a/testsuite/tests/typecheck/should_fail/T11514.stderr b/testsuite/tests/typecheck/should_fail/T11514.stderr
new file mode 100644 (file)
index 0000000..62acf15
--- /dev/null
@@ -0,0 +1,9 @@
+
+T11514.hs:6:7: error:
+    • Cannot instantiate unification variable ‘a0’
+      with a type involving polytypes: (Show a => a -> a) -> ()
+        GHC doesn't yet support impredicative polymorphism
+    • In the expression: undefined
+      In an equation for ‘foo’: foo = undefined
+    • Relevant bindings include
+        foo :: (Show a => a -> a) -> () (bound at T11514.hs:6:1)
index f32e99d..e6619aa 100644 (file)
@@ -1,7 +1,7 @@
 
 T12563.hs:7:15: error:
     • Cannot instantiate unification variable ‘p0’
-      with a type involving foralls: (forall a. f0 a) -> f0 r0
+      with a type involving polytypes: (forall a. f0 a) -> f0 r0
         GHC doesn't yet support impredicative polymorphism
     • In the first argument of ‘foo’, namely ‘g’
       In the expression: foo g
index 5e92f3a..3f380e4 100644 (file)
@@ -3,7 +3,7 @@ T12589.hs:13:3: error: Variable not in scope: (&) :: t1 -> t0 -> t
 
 T12589.hs:13:5: error:
     • Cannot instantiate unification variable ‘t0’
-      with a type involving foralls:
+      with a type involving polytypes:
         (forall a. Bounded a => f0 a) -> h0 f0 xs0
         GHC doesn't yet support impredicative polymorphism
     • In the second argument of ‘(&)’, namely ‘hcpure (Proxy @Bounded)’
index 6344d74..d155ca0 100644 (file)
@@ -390,6 +390,7 @@ test('T11347', normal, compile_fail, [''])
 test('T11356', normal, compile_fail, [''])
 test('T11355', normal, compile_fail, [''])
 test('T11464', normal, compile_fail, [''])
+test('T11514', normal, compile_fail, [''])
 test('T11563', normal, compile_fail, [''])
 test('T11541', normal, compile_fail, [''])
 test('T11313', normal, compile_fail, [''])