[Git][ghc/ghc][wip/T18649] Care with implicit-parameter superclasses

Simon Peyton Jones gitlab at gitlab.haskell.org
Wed Sep 9 09:35:27 UTC 2020



Simon Peyton Jones pushed to branch wip/T18649 at Glasgow Haskell Compiler / GHC


Commits:
2292eeab by Simon Peyton Jones at 2020-09-09T10:28:57+01:00
Care with implicit-parameter superclasses

Two bugs, #18627 and #18649, had the same cause: we were not
account for the fact that a constaint tuple might hide an implicit
parameter.

The solution is not hard: look for implicit parameters in
superclasses.  See Note [Local implicit parameters] in
GHC.Core.Predicate.

Then we use this new function in two places

* The "short-cut solver" in GHC.Tc.Solver.Interact.shortCutSolver
  which simply didn't handle implicit parameters properly at all.
  This fixes #18627

* The specialiser, which should not specialise on implicit parameters
  This fixes #18649

There are some lingering worries (see Note [Local implicit
parameters]) but things are much better.

- - - - -


12 changed files:

- compiler/GHC/Core/Opt/Specialise.hs
- compiler/GHC/Core/Predicate.hs
- compiler/GHC/Tc/Solver.hs
- compiler/GHC/Tc/Solver/Interact.hs
- compiler/GHC/Tc/Solver/Monad.hs
- compiler/GHC/Tc/Utils/TcType.hs
- + testsuite/tests/simplCore/should_compile/T18649.hs
- + testsuite/tests/simplCore/should_compile/T18649.stderr
- testsuite/tests/simplCore/should_compile/all.T
- + testsuite/tests/typecheck/should_run/T18627.hs
- + testsuite/tests/typecheck/should_run/T18627.stdout
- testsuite/tests/typecheck/should_run/all.T


Changes:

=====================================
compiler/GHC/Core/Opt/Specialise.hs
=====================================
@@ -2510,9 +2510,12 @@ mkCallUDs' env f args
     -- we decide on a case by case basis if we want to specialise
     -- on this argument; if so, SpecDict, if not UnspecArg
     mk_spec_arg arg (Anon InvisArg pred)
-      | type_determines_value (scaledThing pred)
-      , interestingDict env arg -- Note [Interesting dictionary arguments]
+      | not (isIPLikePred (scaledThing pred))
+              -- See Note [Type determines value]
+      , interestingDict env arg
+              -- See Note [Interesting dictionary arguments]
       = SpecDict arg
+
       | otherwise = UnspecArg
 
     mk_spec_arg _ (Anon VisArg _)
@@ -2525,41 +2528,18 @@ mkCallUDs' env f args
          -- in specImports
          -- Use 'realIdUnfolding' to ignore the loop-breaker flag!
 
-    type_determines_value pred    -- See Note [Type determines value]
-        = case classifyPredType pred of
-            ClassPred cls _ -> not (isIPClass cls)  -- Superclasses can't be IPs
-            EqPred {}       -> True
-            IrredPred {}    -> True   -- Things like (D []) where D is a
-                                      -- Constraint-ranged family; #7785
-            ForAllPred {}   -> True
-
-{-
-Note [Type determines value]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Only specialise on non-IP *class* params, because these are the ones
-whose *type* determines their *value*.  In particular, with implicit
-params, the type args *don't* say what the value of the implicit param
-is!  See #7101.
+{- Note [Type determines value]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Only specialise on non-impicit-parameter predicates, because these
+are the ones whose *type* determines their *value*.  In particular,
+with implicit params, the type args *don't* say what the value of the
+implicit param is!  See #7101.
 
 So we treat implicit params just like ordinary arguments for the
 purposes of specialisation.  Note that we still want to specialise
 functions with implicit params if they have *other* dicts which are
 class params; see #17930.
 
-One apparent additional complexity involves type families. For
-example, consider
-         type family D (v::*->*) :: Constraint
-         type instance D [] = ()
-         f :: D v => v Char -> Int
-If we see a call (f "foo"), we'll pass a "dictionary"
-  () |> (g :: () ~ D [])
-and it's good to specialise f at this dictionary.
-
-So the question is: can an implicit parameter "hide inside" a
-type-family constraint like (D a).  Well, no.  We don't allow
-        type instance D Maybe = ?x:Int
-Hence the IrredPred case in type_determines_value.  See #7785.
-
 Note [Interesting dictionary arguments]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Consider this


=====================================
compiler/GHC/Core/Predicate.hs
=====================================
@@ -22,7 +22,7 @@ module GHC.Core.Predicate (
   getClassPredTys, getClassPredTys_maybe,
 
   -- Implicit parameters
-  isIPPred, isIPPred_maybe, isIPTyCon, isIPClass, hasIPPred,
+  isIPLikePred, hasIPSuperClasses, isIPTyCon, isIPClass,
 
   -- Evidence variables
   DictId, isEvVar, isDictId
@@ -39,12 +39,10 @@ import GHC.Core.Multiplicity ( scaledThing )
 
 import GHC.Builtin.Names
 
-import GHC.Data.FastString
 import GHC.Utils.Outputable
 import GHC.Utils.Misc
 import GHC.Utils.Panic
 
-import Control.Monad ( guard )
 
 -- | A predicate in the solver. The solver tries to prove Wanted predicates
 -- from Given ones.
@@ -170,7 +168,7 @@ isEqPredClass :: Class -> Bool
 isEqPredClass cls =  cls `hasKey` eqTyConKey
                   || cls `hasKey` heqTyConKey
 
-isClassPred, isEqPred, isEqPrimPred, isIPPred :: PredType -> Bool
+isClassPred, isEqPred, isEqPrimPred :: PredType -> Bool
 isClassPred ty = case tyConAppTyCon_maybe ty of
     Just tyCon | isClassTyCon tyCon -> True
     _                               -> False
@@ -186,9 +184,15 @@ isEqPred ty  -- True of (a ~ b) and (a ~~ b)
 isEqPrimPred ty = isCoVarType ty
   -- True of (a ~# b) (a ~R# b)
 
-isIPPred ty = case tyConAppTyCon_maybe ty of
-    Just tc -> isIPTyCon tc
-    _       -> False
+isCTupleClass :: Class -> Bool
+isCTupleClass cls = isTupleTyCon (classTyCon cls)
+
+
+{- *********************************************************************
+*                                                                      *
+              Implicit parameters
+*                                                                      *
+********************************************************************* -}
 
 isIPTyCon :: TyCon -> Bool
 isIPTyCon tc = tc `hasKey` ipClassKey
@@ -197,31 +201,105 @@ isIPTyCon tc = tc `hasKey` ipClassKey
 isIPClass :: Class -> Bool
 isIPClass cls = cls `hasKey` ipClassKey
 
-isCTupleClass :: Class -> Bool
-isCTupleClass cls = isTupleTyCon (classTyCon cls)
+isIPLikePred :: Type -> Bool
+-- See Note [Local implicit parameters]
+isIPLikePred = is_ip_like_pred initIPRecTc
 
-isIPPred_maybe :: Type -> Maybe (FastString, Type)
-isIPPred_maybe ty =
-  do (tc,[t1,t2]) <- splitTyConApp_maybe ty
-     guard (isIPTyCon tc)
-     x <- isStrLitTy t1
-     return (x,t2)
-
-hasIPPred :: PredType -> Bool
-hasIPPred pred
-  = case classifyPredType pred of
-      ClassPred cls tys
-        | isIPClass     cls -> True
-        | isCTupleClass cls -> any hasIPPred tys
-      _other -> False
 
-{-
-************************************************************************
+is_ip_like_pred :: RecTcChecker -> Type -> Bool
+is_ip_like_pred rec_clss ty
+  | Just (tc, tys) <- splitTyConApp_maybe ty
+  , Just rec_clss' <- if isTupleTyCon tc  -- Tuples never cause recursion
+                      then Just rec_clss
+                      else checkRecTc rec_clss tc
+  , Just cls       <- tyConClass_maybe tc
+  = isIPClass cls || has_ip_super_classes rec_clss' cls tys
+
+  | otherwise
+  = False -- Includes things like (D []) where D is
+          -- a Constraint-ranged family; #7785
+
+hasIPSuperClasses :: Class -> [Type] -> Bool
+-- See Note [Local implicit parameters]
+hasIPSuperClasses = has_ip_super_classes initIPRecTc
+
+has_ip_super_classes :: RecTcChecker -> Class -> [Type] -> Bool
+has_ip_super_classes rec_clss cls tys
+  = any ip_ish (classSCSelIds cls)
+  where
+    -- Check that the type of a superclass determines its value
+    -- sc_sel_id :: forall a b. C a b -> <superclass type>
+    ip_ish sc_sel_id = is_ip_like_pred rec_clss $
+                       funResultTy              $
+                       piResultTys (varType sc_sel_id) tys
+
+
+initIPRecTc :: RecTcChecker
+initIPRecTc = setRecTcMaxBound 1 initRecTc
+
+{- Note [Local implicit parameters]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+The function isIPLikePred tells if this predicate, or any of its
+superclasses, is an implicit parameter.
+
+Why are implicit parameters special?  Unlike normal classes, we can
+have local instances for implicit parameters, in the form of
+   let ?x = True in ...
+So in various places we must be careful not to assume that any value
+of the right type will do; we must carefully look for the innermost binding.
+So isIPLikePred checks whether this is an implicit parameter, or has
+a superclass that is an implicit parameter.
+
+Several wrinkles
+
+* We must be careful with superclasses, as #18649 showed.  Haskell
+  doesn't allow an implicit parameter as a superclass
+    class (?x::a) => C a where ...
+  but with a constraint tuple we might have
+     (% Eq a, ?x::Int %)
+  and /its/ superclasses, namely (Eq a) and (?x::Int), /do/ include an
+  implicit parameter.
+
+  With ConstraintKinds this can apply to /any/ class, e.g.
+     class sc => C sc where ...
+  Then (C (?x::Int)) has (?x::Int) as a superclass.  So we must
+  instantiate and check each superclass, one by one, in
+  hasIPSuperClasses.
+
+* With -XRecursiveSuperClasses, the superclass hunt can go on forever,
+  so we need a RecTcChecker to cut it off.
+
+* Another apparent additional complexity involves type families. For
+  example, consider
+         type family D (v::*->*) :: Constraint
+         type instance D [] = ()
+         f :: D v => v Char -> Int
+  If we see a call (f "foo"), we'll pass a "dictionary"
+    () |> (g :: () ~ D [])
+  and it's good to specialise f at this dictionary.
+
+So the question is: can an implicit parameter "hide inside" a
+type-family constraint like (D a).  Well, no.  We don't allow
+        type instance D Maybe = ?x:Int
+Hence the umbrella 'otherwise' case in is_ip_like_pred.  See #7785.
+
+Small worries (Sept 20):
+* I don't see what stops us having that 'type instance'. Indeed I
+  think nothing does.
+* I'm a little concerned about type variables; such a variable might
+  be instantiated to an implicit parameter.  I don't think this
+  matters in the cases for which isIPLikePred is used, and it's pretty
+  obscure anyway.
+* The superclass hunt stops when it encounters the same class again,
+  but in principle we could have the same class, differently instantiated,
+  and the second time it could have an implicit parameter
+I'm going to treat these as problems for another day. They are all exotic.  -}
+
+{- *********************************************************************
 *                                                                      *
               Evidence variables
 *                                                                      *
-************************************************************************
--}
+********************************************************************* -}
 
 isEvVar :: Var -> Bool
 isEvVar var = isEvVarType (varType var)


=====================================
compiler/GHC/Tc/Solver.hs
=====================================
@@ -1377,7 +1377,7 @@ growThetaTyVars theta tcvs
   | otherwise  = transCloVarSet mk_next seed_tcvs
   where
     seed_tcvs = tcvs `unionVarSet` tyCoVarsOfTypes ips
-    (ips, non_ips) = partition isIPPred theta
+    (ips, non_ips) = partition isIPLikePred theta
                          -- See Note [Inheriting implicit parameters] in GHC.Tc.Utils.TcType
 
     mk_next :: VarSet -> VarSet -- Maps current set to newly-grown ones


=====================================
compiler/GHC/Tc/Solver/Interact.hs
=====================================
@@ -566,10 +566,10 @@ solveOneFromTheOther ev_i ev_w
      ev_id_w = ctEvEvId ev_w
 
      different_level_strategy  -- Both Given
-       | isIPPred pred = if lvl_w > lvl_i then KeepWork  else KeepInert
-       | otherwise     = if lvl_w > lvl_i then KeepInert else KeepWork
+       | isIPLikePred pred = if lvl_w > lvl_i then KeepWork  else KeepInert
+       | otherwise         = if lvl_w > lvl_i then KeepInert else KeepWork
        -- See Note [Replacement vs keeping] (the different-level bullet)
-       -- For the isIPPred case see Note [Shadowing of Implicit Parameters]
+       -- For the isIPLikePred case see Note [Shadowing of Implicit Parameters]
 
      same_level_strategy binds -- Both Given
        | GivenOrigin (InstSC s_i) <- ctLocOrigin loc_i
@@ -1071,6 +1071,8 @@ shortCutSolver dflags ev_w ev_i
  -- programs should typecheck regardless of whether we take this step or
  -- not. See Note [Shortcut solving]
 
+ && not (isIPLikePred (ctEvPred ev_w))   -- Not for implicit parameters (#18627)
+
  && not (xopt LangExt.IncoherentInstances dflags)
  -- If IncoherentInstances is on then we cannot rely on coherence of proofs
  -- in order to justify this optimization: The proof provided by the
@@ -1079,6 +1081,7 @@ shortCutSolver dflags ev_w ev_i
 
  && gopt Opt_SolveConstantDicts dflags
  -- Enabled by the -fsolve-constant-dicts flag
+
   = do { ev_binds_var <- getTcEvBindsVar
        ; ev_binds <- ASSERT2( not (isCoEvBindsVar ev_binds_var ), ppr ev_w )
                      getTcEvBindsMap ev_binds_var


=====================================
compiler/GHC/Tc/Solver/Monad.hs
=====================================
@@ -2527,8 +2527,7 @@ emptyDictMap = emptyTcAppMap
 
 findDict :: DictMap a -> CtLoc -> Class -> [Type] -> Maybe a
 findDict m loc cls tys
-  | isCTupleClass cls
-  , any hasIPPred tys   -- See Note [Tuples hiding implicit parameters]
+  | hasIPSuperClasses cls tys -- See Note [Tuples hiding implicit parameters]
   = Nothing
 
   | Just {} <- isCallStackPred cls tys


=====================================
compiler/GHC/Tc/Utils/TcType.hs
=====================================
@@ -79,7 +79,7 @@ module GHC.Tc.Utils.TcType (
   isFloatingTy, isDoubleTy, isFloatTy, isIntTy, isWordTy, isStringTy,
   isIntegerTy, isNaturalTy,
   isBoolTy, isUnitTy, isCharTy, isCallStackTy, isCallStackPred,
-  hasIPPred, isTauTy, isTauTyCon, tcIsTyVarTy, tcIsForAllTy,
+  isTauTy, isTauTyCon, tcIsTyVarTy, tcIsForAllTy,
   isPredTy, isTyVarClassPred, isTyVarHead, isInsolubleOccursCheck,
   checkValidClsArgs, hasTyVarHead,
   isRigidTy, isAlmostFunctionFree,
@@ -141,7 +141,7 @@ module GHC.Tc.Utils.TcType (
   mkTyConTy, mkTyVarTy, mkTyVarTys,
   mkTyCoVarTy, mkTyCoVarTys,
 
-  isClassPred, isEqPrimPred, isIPPred, isEqPred, isEqPredClass,
+  isClassPred, isEqPrimPred, isIPLikePred, isEqPred, isEqPredClass,
   mkClassPred,
   tcSplitDFunTy, tcSplitDFunHead, tcSplitMethodTy,
   isRuntimeRepVar, isKindLevPoly,
@@ -1747,7 +1747,7 @@ pickCapturedPreds
 pickCapturedPreds qtvs theta
   = filter captured theta
   where
-    captured pred = isIPPred pred || (tyCoVarsOfType pred `intersectsVarSet` qtvs)
+    captured pred = isIPLikePred pred || (tyCoVarsOfType pred `intersectsVarSet` qtvs)
 
 
 -- Superclasses


=====================================
testsuite/tests/simplCore/should_compile/T18649.hs
=====================================
@@ -0,0 +1,26 @@
+{-# LANGUAGE ImplicitParams #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE FlexibleContexts #-}
+
+module Test where
+
+import Prelude
+
+type Hidden a =
+  ( ?enable :: a
+  , Eq a  -- removing this "fixes" the issue
+  )
+
+{-# NOINLINE a #-}
+a :: Hidden Bool => Integer -> Bool
+a _ = ?enable
+
+system :: Hidden Bool => Bool
+system = a 0
+
+topEntity :: Bool -> Bool
+topEntity ena = let ?enable = ena
+                in system
+
+someVar = let ?enable = True
+          in system


=====================================
testsuite/tests/simplCore/should_compile/T18649.stderr
=====================================
@@ -0,0 +1,4 @@
+
+==================== Tidy Core rules ====================
+
+


=====================================
testsuite/tests/simplCore/should_compile/all.T
=====================================
@@ -333,3 +333,7 @@ test('T18347', normal, compile, ['-dcore-lint -O'])
 test('T18355', [ grep_errmsg(r'OneShot') ], compile, ['-O -ddump-simpl -dsuppress-uniques'])
 test('T18399', normal, compile, ['-dcore-lint -O'])
 test('T18589', normal, compile, ['-dcore-lint -O'])
+
+# T18648 should /not/ generate a specialisation rule
+test('T18649', normal, compile, ['-O -ddump-rules -Wno-simplifiable-class-constraints'])
+


=====================================
testsuite/tests/typecheck/should_run/T18627.hs
=====================================
@@ -0,0 +1,16 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE ImplicitParams #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+module Main where
+
+import GHC.Classes
+
+instance IP "x" Int where
+  ip = 21
+
+baz :: (?x :: Int) => Int
+baz = ?x
+
+main :: IO ()
+main  = let ?x = 42
+        in print baz


=====================================
testsuite/tests/typecheck/should_run/T18627.stdout
=====================================
@@ -0,0 +1 @@
+42


=====================================
testsuite/tests/typecheck/should_run/all.T
=====================================
@@ -146,3 +146,4 @@ test('UnliftedNewtypesDependentFamilyRun', normal, compile_and_run, [''])
 test('UnliftedNewtypesIdentityRun', normal, compile_and_run, [''])
 test('UnliftedNewtypesCoerceRun', normal, compile_and_run, [''])
 test('T17104', normal, compile_and_run, [''])
+test('T18627', normal, compile_and_run, ['-O'])  # Optimisation shows up the bug



View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/2292eeab80ac065ac33c155908b7883898f98be9

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/2292eeab80ac065ac33c155908b7883898f98be9
You're receiving this email because of your account on gitlab.haskell.org.


-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-commits/attachments/20200909/affc64f7/attachment-0001.html>


More information about the ghc-commits mailing list