[Git][ghc/ghc][ghc-9.0] 4 commits: Care with implicit-parameter superclasses

Ben Gamari gitlab at gitlab.haskell.org
Wed Oct 14 18:11:04 UTC 2020



Ben Gamari pushed to branch ghc-9.0 at Glasgow Haskell Compiler / GHC


Commits:
7e257575 by Simon Peyton Jones at 2020-10-13T23:35:26+02: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.

(cherry picked from commit c7182a5c67fe8b5bd256cb8eb805562636853ea2)

- - - - -
9060a9dd by Ben Gamari at 2020-10-13T23:36:56+02:00
sdist: Include hadrian sources in source distribution

Previously the make build system's source distribution rules neglected
to include Hadrian's sources.

Fixes #18794.

(cherry picked from commit 9657f6f34a1a00008a0db935dbf25733cb483cd4)

- - - - -
fb5eb8ab by Simon Peyton Jones at 2020-10-13T23:37:29+02:00
Fix desugaring of record updates on data families

This fixes a long-standing bug in the desugaring of record
updates for data families, when the latter involves a GADT. It's
all explained in Note [Update for GADTs] in GHC.HsToCore.Expr.

Building the correct cast is surprisingly tricky, as that Note
explains.

Fixes #18809.  The test case (in indexed-types/should_compile/T18809)
contains several examples that exercise the dark corners.

(cherry picked from commit bfdccac6acce84e15292a454d12f4e0d87ef6f10)

- - - - -
64ab97bf by Krzysztof Gogolewski at 2020-10-13T23:39:06+02:00
Add -pgmlm and -optlm flags

!3798 added documentation and semantics for the flags,
but not parsing.

(cherry picked from commit fd302e938ebf48c73d9f715d67ce8cd990f972ff)

- - - - -


26 changed files:

- compiler/GHC/Core/Coercion.hs
- compiler/GHC/Core/DataCon.hs
- compiler/GHC/Core/Opt/Specialise.hs
- compiler/GHC/Core/Predicate.hs
- compiler/GHC/Core/TyCo/Subst.hs
- compiler/GHC/Driver/Session.hs
- compiler/GHC/Hs/Expr.hs
- compiler/GHC/HsToCore/Expr.hs
- compiler/GHC/Tc/Instance/Class.hs
- compiler/GHC/Tc/Module.hs
- compiler/GHC/Tc/Solver.hs
- compiler/GHC/Tc/Solver/Canonical.hs
- compiler/GHC/Tc/Solver/Interact.hs
- compiler/GHC/Tc/Solver/Monad.hs
- compiler/GHC/Tc/TyCl/Instance.hs
- compiler/GHC/Tc/Types/Evidence.hs
- compiler/GHC/Tc/Utils/TcType.hs
- ghc.mk
- + testsuite/tests/indexed-types/should_compile/T18809.hs
- testsuite/tests/indexed-types/should_compile/all.T
- + 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/Coercion.hs
=====================================
@@ -41,6 +41,7 @@ module GHC.Core.Coercion (
         downgradeRole, mkAxiomRuleCo,
         mkGReflRightCo, mkGReflLeftCo, mkCoherenceLeftCo, mkCoherenceRightCo,
         mkKindCo, castCoercionKind, castCoercionKindI,
+        mkFamilyTyConAppCo,
 
         mkHeteroCoercionType,
         mkPrimEqPred, mkReprPrimEqPred, mkPrimEqPredRole,
@@ -1505,6 +1506,27 @@ castCoercionKindI g h1 h2
   = mkCoherenceRightCo r t2 h2 (mkCoherenceLeftCo r t1 h1 g)
   where (Pair t1 t2, r) = coercionKindRole g
 
+mkFamilyTyConAppCo :: TyCon -> [CoercionN] -> CoercionN
+-- ^ Given a family instance 'TyCon' and its arg 'Coercion's, return the
+-- corresponding family 'Coercion'.  E.g:
+--
+-- > data family T a
+-- > data instance T (Maybe b) = MkT b
+--
+-- Where the instance 'TyCon' is :RTL, so:
+--
+-- > mkFamilyTyConAppCo :RTL (co :: a ~# Int) = T (Maybe a) ~# T (Maybe Int)
+--
+-- cf. 'mkFamilyTyConApp'
+mkFamilyTyConAppCo tc cos
+  | Just (fam_tc, fam_tys) <- tyConFamInst_maybe tc
+  , let tvs = tyConTyVars tc
+        fam_cos = ASSERT2( tvs `equalLength` cos, ppr tc <+> ppr cos )
+                  map (liftCoSubstWith Nominal tvs cos) fam_tys
+  = mkTyConAppCo Nominal fam_tc fam_cos
+  | otherwise
+  = mkTyConAppCo Nominal tc cos
+
 -- See note [Newtype coercions] in GHC.Core.TyCon
 
 mkPiCos :: Role -> [Var] -> Coercion -> Coercion


=====================================
compiler/GHC/Core/DataCon.hs
=====================================
@@ -580,6 +580,7 @@ variables:
   purposes of TypeApplications, and as a consequence, they do not come equipped
   with visibilities (that is, they are TyVars/TyCoVars instead of
   TyCoVarBinders).
+
 * dcUserTyVarBinders, for the type variables binders in the order in which they
   originally arose in the user-written type signature. Their order *does* matter
   for TypeApplications, so they are full TyVarBinders, complete with
@@ -600,10 +601,10 @@ dcExTyCoVars. That is, the tyvars in dcUserTyVarBinders are a permutation of
 ordering, they in fact share the same type variables (with the same Uniques). We
 sometimes refer to this as "the dcUserTyVarBinders invariant".
 
-dcUserTyVarBinders, as the name suggests, is the one that users will see most of
-the time. It's used when computing the type signature of a data constructor (see
-dataConWrapperType), and as a result, it's what matters from a TypeApplications
-perspective.
+dcUserTyVarBinders, as the name suggests, is the one that users will
+see most of the time. It's used when computing the type signature of a
+data constructor wrapper (see dataConWrapperType), and as a result,
+it's what matters from a TypeApplications perspective.
 
 Note [The dcEqSpec domain invariant]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~


=====================================
compiler/GHC/Core/Opt/Specialise.hs
=====================================
@@ -2508,9 +2508,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 _)
@@ -2523,41 +2526,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
=====================================
@@ -20,9 +20,10 @@ module GHC.Core.Predicate (
   mkClassPred, isDictTy,
   isClassPred, isEqPredClass, isCTupleClass,
   getClassPredTys, getClassPredTys_maybe,
+  classMethodTy, classMethodInstTy,
 
   -- Implicit parameters
-  isIPPred, isIPPred_maybe, isIPTyCon, isIPClass, hasIPPred,
+  isIPLikePred, hasIPSuperClasses, isIPTyCon, isIPClass,
 
   -- Evidence variables
   DictId, isEvVar, isDictId
@@ -38,12 +39,10 @@ import GHC.Core.Coercion
 
 import GHC.Builtin.Names
 
-import GHC.Data.FastString
 import GHC.Utils.Outputable
 import GHC.Utils.Misc
 import GHC.Core.Multiplicity ( scaledThing )
 
-import Control.Monad ( guard )
 
 -- | A predicate in the solver. The solver tries to prove Wanted predicates
 -- from Given ones.
@@ -94,6 +93,26 @@ getClassPredTys_maybe ty = case splitTyConApp_maybe ty of
         Just (tc, tys) | Just clas <- tyConClass_maybe tc -> Just (clas, tys)
         _ -> Nothing
 
+classMethodTy :: Id -> Type
+-- Takes a class selector op :: forall a. C a => meth_ty
+-- and returns the type of its method, meth_ty
+-- The selector can be a superclass selector, in which case
+-- you get back a superclass
+classMethodTy sel_id
+  = funResultTy $        -- meth_ty
+    dropForAlls $        -- C a => meth_ty
+    varType sel_id        -- forall a. C n => meth_ty
+
+classMethodInstTy :: Id -> [Type] -> Type
+-- Takes a class selector op :: forall a b. C a b => meth_ty
+-- and the types [ty1, ty2] at which it is instantiated,
+-- returns the instantiated type of its method, meth_ty[t1/a,t2/b]
+-- The selector can be a superclass selector, in which case
+-- you get back a superclass
+classMethodInstTy sel_id arg_tys
+  = funResultTy $
+    piResultTys (varType sel_id) arg_tys
+
 -- --------------------- Equality predicates ---------------------------------
 
 -- | A choice of equality relation. This is separate from the type 'Role'
@@ -169,7 +188,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
@@ -185,9 +204,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
@@ -196,31 +221,103 @@ 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 $
+                       classMethodInstTy 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/Core/TyCo/Subst.hs
=====================================
@@ -435,8 +435,8 @@ mkTvSubstPrs prs =
 zipTyEnv :: HasDebugCallStack => [TyVar] -> [Type] -> TvSubstEnv
 zipTyEnv tyvars tys
   | debugIsOn
-  , not (all isTyVar tyvars)
-  = pprPanic "zipTyEnv" (ppr tyvars <+> ppr tys)
+  , not (all isTyVar tyvars && (tyvars `equalLength` tys))
+  = pprPanic "zipTyEnv" (ppr tyvars $$ ppr tys)
   | otherwise
   = ASSERT( all (not . isCoercionTy) tys )
     mkVarEnv (zipEqual "zipTyEnv" tyvars tys)


=====================================
compiler/GHC/Driver/Session.hs
=====================================
@@ -2360,6 +2360,8 @@ dynamic_flags_deps = [
       $ hasArg $ \f -> alterToolSettings $ \s -> s { toolSettings_pgm_lo  = (f,[]) }
   , make_ord_flag defFlag "pgmlc"
       $ hasArg $ \f -> alterToolSettings $ \s -> s { toolSettings_pgm_lc  = (f,[]) }
+  , make_ord_flag defFlag "pgmlm"
+      $ hasArg $ \f -> alterToolSettings $ \s -> s { toolSettings_pgm_lm  = (f,[]) }
   , make_ord_flag defFlag "pgmi"
       $ hasArg $ \f -> alterToolSettings $ \s -> s { toolSettings_pgm_i   =  f }
   , make_ord_flag defFlag "pgmL"
@@ -2396,6 +2398,8 @@ dynamic_flags_deps = [
 
 
     -- need to appear before -optl/-opta to be parsed as LLVM flags.
+  , make_ord_flag defFlag "optlm"
+      $ hasArg $ \f -> alterToolSettings $ \s -> s { toolSettings_opt_lm  = f : toolSettings_opt_lm s }
   , make_ord_flag defFlag "optlo"
       $ hasArg $ \f -> alterToolSettings $ \s -> s { toolSettings_opt_lo  = f : toolSettings_opt_lo s }
   , make_ord_flag defFlag "optlc"


=====================================
compiler/GHC/Hs/Expr.hs
=====================================
@@ -574,8 +574,9 @@ data RecordUpdTc = RecordUpdTc
 
       , rupd_in_tys  :: [Type]  -- Argument types of *input* record type
       , rupd_out_tys :: [Type]  --             and  *output* record type
-                                -- The original type can be reconstructed
-                                -- with conLikeResTy
+                -- For a data family, these are the type args of the
+                -- /representation/ type constructor
+
       , rupd_wrap :: HsWrapper  -- See note [Record Update HsWrapper]
       }
 


=====================================
compiler/GHC/HsToCore/Expr.hs
=====================================
@@ -46,6 +46,7 @@ import GHC.Tc.Types.Evidence
 import GHC.Tc.Utils.Monad
 import GHC.Core.Type
 import GHC.Core.Multiplicity
+import GHC.Core.Coercion( Coercion )
 import GHC.Core
 import GHC.Core.Utils
 import GHC.Core.Make
@@ -54,6 +55,7 @@ import GHC.Driver.Session
 import GHC.Types.CostCentre
 import GHC.Types.Id
 import GHC.Types.Id.Make
+import GHC.Types.Var.Env
 import GHC.Unit.Module
 import GHC.Core.ConLike
 import GHC.Core.DataCon
@@ -62,13 +64,11 @@ import GHC.Builtin.Types
 import GHC.Builtin.Names
 import GHC.Types.Basic
 import GHC.Data.Maybe
-import GHC.Types.Var.Env
 import GHC.Types.SrcLoc
 import GHC.Utils.Misc
 import GHC.Data.Bag
 import GHC.Utils.Outputable as Outputable
 import GHC.Core.PatSyn
-
 import Control.Monad
 import Data.List.NonEmpty ( nonEmpty )
 
@@ -614,13 +614,70 @@ Note [Update for GADTs]
 ~~~~~~~~~~~~~~~~~~~~~~~
 Consider
    data T a b where
-     T1 :: { f1 :: a } -> T a Int
+     MkT :: { foo :: a } -> T a Int
+
+   upd :: T s t -> s -> T s t
+   upd z y = z { foo = y}
+
+We need to get this:
+   $WMkT :: a -> T a Int
+   MkT   :: (b ~# Int) => a -> T a b
+
+   upd = /\s t. \(z::T s t) (y::s) ->
+         case z of
+            MkT (co :: t ~# Int) _ -> $WMkT @s y |> T (Refl s) (Sym co)
 
-Then the wrapper function for T1 has type
-   $WT1 :: a -> T a Int
-But if x::T a b, then
-   x { f1 = v } :: T a b   (not T a Int!)
-So we need to cast (T a Int) to (T a b).  Sigh.
+Note the final cast
+   T (Refl s) (Sym co) :: T s Int ~ T s t
+which uses co, bound by the GADT match.  This is the wrap_co coercion
+in wrapped_rhs. How do we produce it?
+
+* Start with raw materials
+    tc, the tycon:                                       T
+    univ_tvs, the universally quantified tyvars of MkT:  a,b
+  NB: these are in 1-1 correspondence with the tyvars of tc
+
+* Form univ_cos, a coercion for each of tc's args: (Refl s) (Sym co)
+  We replaced
+     a  by  (Refl s)    since 's' instantiates 'a'
+     b  by  (Sym co)   since 'b' is in the data-con's EqSpec
+
+* Then form the coercion T (Refl s) (Sym co)
+
+It gets more complicated when data families are involved (#18809).
+Consider
+    data family F x
+    data instance F (a,b) where
+      MkF :: { foo :: Int } -> F (Int,b)
+
+    bar :: F (s,t) -> Int -> F (s,t)
+    bar z y = z { foo = y}
+
+We have
+    data R:FPair a b where
+      MkF :: { foo :: Int } -> R:FPair Int b
+
+    $WMkF :: Int -> F (Int,b)
+    MkF :: forall a b. (a ~# Int) => Int -> R:FPair a b
+
+    bar :: F (s,t) -> Int -> F (s,t)
+    bar = /\s t. \(z::F (s,t)) \(y::Int) ->
+         case z |> co1 of
+            MkF (co2::s ~# Int) _ -> $WMkF @t y |> co3
+
+(Side note: here (z |> co1) is built by typechecking the scrutinee, so
+we ignore it here.  In general the scrutinee is an aribtrary expression.)
+
+The question is: what is co3, the cast for the RHS?
+      co3 :: F (Int,t) ~ F (s,t)
+Again, we can construct it using co2, bound by the GADT match.
+We do /exactly/ the same as the non-family case up to building
+univ_cos.  But that gives us
+     rep_tc:   R:FPair
+     univ_cos: (Sym co2)   (Refl t)
+But then we use mkTcFamilyTyConAppCo to "lift" this to the coercion
+we want, namely
+     F (Sym co2, Refl t) :: F (Int,t) ~ F (s,t)
 
 -}
 
@@ -707,8 +764,7 @@ dsExpr expr@(RecordUpd { rupd_expr = record_expr, rupd_flds = fields
                         dict_req_wrap                                           <.>
                         mkWpTyApps    [ lookupTyVar out_subst tv
                                           `orElse` mkTyVarTy tv
-                                      | tv <- user_tvs
-                                      , not (tv `elemVarEnv` wrap_subst) ]
+                                      | tv <- user_tvs ]
                           -- Be sure to use user_tvs (which may be ordered
                           -- differently than `univ_tvs ++ ex_tvs) above.
                           -- See Note [DataCon user type variable binders]
@@ -719,27 +775,30 @@ dsExpr expr@(RecordUpd { rupd_expr = record_expr, rupd_flds = fields
                         -- Note [Update for GADTs]
                  wrapped_rhs =
                   case con of
-                    RealDataCon data_con ->
-                      let
-                        wrap_co =
-                          mkTcTyConAppCo Nominal
-                            (dataConTyCon data_con)
-                            [ lookup tv ty
-                              | (tv,ty) <- univ_tvs `zip` out_inst_tys ]
-                        lookup univ_tv ty =
-                          case lookupVarEnv wrap_subst univ_tv of
-                            Just co' -> co'
-                            Nothing  -> mkTcReflCo Nominal ty
-                        in if null eq_spec
-                             then rhs
-                             else mkLHsWrap (mkWpCastN wrap_co) rhs
+                    RealDataCon data_con
+                      | null eq_spec -> rhs
+                      | otherwise    -> mkLHsWrap (mkWpCastN wrap_co) rhs
+                                     -- This wrap is the punchline: Note [Update for GADTs]
+                      where
+                        rep_tc   = dataConTyCon data_con
+                        wrap_co  = mkTcFamilyTyConAppCo rep_tc univ_cos
+                        univ_cos = zipWithEqual "dsExpr:upd" mk_univ_co univ_tvs out_inst_tys
+
+                        mk_univ_co :: TyVar   -- Universal tyvar from the DataCon
+                                   -> Type    -- Corresponding instantiating type
+                                   -> Coercion
+                        mk_univ_co univ_tv inst_ty
+                          = case lookupVarEnv eq_spec_env univ_tv of
+                               Just co -> co
+                               Nothing -> mkTcNomReflCo inst_ty
+
+                        eq_spec_env :: VarEnv Coercion
+                        eq_spec_env = mkVarEnv [ (eqSpecTyVar spec, mkTcSymCo (mkTcCoVarCo eqs_var))
+                                               | (spec,eqs_var) <- zipEqual "dsExpr:upd2" eq_spec eqs_vars ]
+
                     -- eq_spec is always null for a PatSynCon
                     PatSynCon _ -> rhs
 
-                 wrap_subst =
-                  mkVarEnv [ (tv, mkTcSymCo (mkTcCoVarCo eq_var))
-                           | (spec, eq_var) <- eq_spec `zip` eqs_vars
-                           , let tv = eqSpecTyVar spec ]
 
                  req_wrap = dict_req_wrap <.> mkWpTyApps in_inst_tys
 


=====================================
compiler/GHC/Tc/Instance/Class.hs
=====================================
@@ -387,10 +387,9 @@ makeLitDict clas ty et
     | Just (_, co_dict) <- tcInstNewTyCon_maybe (classTyCon clas) [ty]
           -- co_dict :: KnownNat n ~ SNat n
     , [ meth ]   <- classMethods clas
-    , Just tcRep <- tyConAppTyCon_maybe -- SNat
-                      $ funResultTy         -- SNat n
-                      $ dropForAlls         -- KnownNat n => SNat n
-                      $ idType meth         -- forall n. KnownNat n => SNat n
+    , Just tcRep <- tyConAppTyCon_maybe (classMethodTy meth)
+                    -- If the method type is forall n. KnownNat n => SNat n
+                    -- then tcRep is SNat
     , Just (_, co_rep) <- tcInstNewTyCon_maybe tcRep [ty]
           -- SNat n ~ Integer
     , let ev_tm = mkEvCast et (mkTcSymCo (mkTcTransCo co_dict co_rep))


=====================================
compiler/GHC/Tc/Module.hs
=====================================
@@ -65,9 +65,10 @@ import GHC.Builtin.Types ( unitTy, mkListTy )
 import GHC.Driver.Plugins
 import GHC.Driver.Session
 import GHC.Hs
-import GHC.Iface.Syntax ( ShowSub(..), showToHeader )
-import GHC.Iface.Type   ( ShowForAllFlag(..) )
-import GHC.Core.PatSyn( pprPatSynType )
+import GHC.Iface.Syntax   ( ShowSub(..), showToHeader )
+import GHC.Iface.Type     ( ShowForAllFlag(..) )
+import GHC.Core.PatSyn    ( pprPatSynType )
+import GHC.Core.Predicate ( classMethodTy )
 import GHC.Builtin.Names
 import GHC.Builtin.Utils
 import GHC.Types.Name.Reader
@@ -1014,10 +1015,8 @@ checkBootTyCon is_boot tc1 tc2
           name2 = idName id2
           pname1 = quotes (ppr name1)
           pname2 = quotes (ppr name2)
-          (_, rho_ty1) = splitForAllTys (idType id1)
-          op_ty1 = funResultTy rho_ty1
-          (_, rho_ty2) = splitForAllTys (idType id2)
-          op_ty2 = funResultTy rho_ty2
+          op_ty1 = classMethodTy id1
+          op_ty2 = classMethodTy id2
 
        eqAT (ATI tc1 def_ats1) (ATI tc2 def_ats2)
          = checkBootTyCon is_boot tc1 tc2 `andThenCheck`


=====================================
compiler/GHC/Tc/Solver.hs
=====================================
@@ -1376,7 +1376,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/Canonical.hs
=====================================
@@ -29,7 +29,7 @@ import GHC.Core.Multiplicity
 import GHC.Core.TyCo.Rep   -- cleverly decomposes types, good for completeness checking
 import GHC.Core.Coercion
 import GHC.Core
-import GHC.Types.Id( idType, mkTemplateLocals )
+import GHC.Types.Id( mkTemplateLocals )
 import GHC.Core.FamInstEnv ( FamInstEnvs )
 import GHC.Tc.Instance.Family ( tcTopNormaliseNewTypeTF_maybe )
 import GHC.Types.Var
@@ -541,7 +541,7 @@ mk_strict_superclasses rec_clss (CtGiven { ctev_evar = evar, ctev_loc = loc })
                          mk_given_desc sel_id sc_pred
            ; mk_superclasses rec_clss given_ev tvs theta sc_pred }
       where
-        sc_pred  = funResultTy (piResultTys (idType sel_id) tys)
+        sc_pred = classMethodInstTy sel_id tys
 
       -- See Note [Nested quantified constraint superclasses]
     mk_given_desc :: Id -> PredType -> (PredType, EvTerm)


=====================================
compiler/GHC/Tc/Solver/Interact.hs
=====================================
@@ -565,10 +565,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
@@ -1070,6 +1070,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
@@ -1078,6 +1080,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
=====================================
@@ -2526,8 +2526,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/TyCl/Instance.hs
=====================================
@@ -53,6 +53,7 @@ import GHC.Core        ( Expr(..), mkApps, mkVarApps, mkLams )
 import GHC.Core.Make   ( nO_METHOD_BINDING_ERROR_ID )
 import GHC.Core.Unfold ( mkInlineUnfoldingWithArity, mkDFunUnfolding )
 import GHC.Core.Type
+import GHC.Core.Predicate( classMethodInstTy )
 import GHC.Tc.Types.Evidence
 import GHC.Core.TyCon
 import GHC.Core.Coercion.Axiom
@@ -1631,7 +1632,7 @@ tcMethods dfun_id clas tyvars dfun_ev_vars inst_tys
                               nO_METHOD_BINDING_ERROR_ID
         error_msg dflags = L inst_loc (HsLit noExtField (HsStringPrim NoSourceText
                                               (unsafeMkByteString (error_string dflags))))
-        meth_tau     = funResultTy (piResultTys (idType sel_id) inst_tys)
+        meth_tau     = classMethodInstTy sel_id inst_tys
         error_string dflags = showSDoc dflags
                               (hcat [ppr inst_loc, vbar, ppr sel_id ])
         lam_wrapper  = mkWpTyLams tyvars <.> mkWpLams dfun_ev_vars


=====================================
compiler/GHC/Tc/Types/Evidence.hs
=====================================
@@ -48,6 +48,7 @@ module GHC.Tc.Types.Evidence (
   mkTcKindCo,
   tcCoercionKind,
   mkTcCoVarCo,
+  mkTcFamilyTyConAppCo,
   isTcReflCo, isTcReflexiveCo,
   tcCoercionRole,
   unwrapIP, wrapIP,
@@ -139,6 +140,7 @@ mkTcCoherenceRightCo   :: Role -> TcType -> TcCoercionN
 mkTcPhantomCo          :: TcCoercionN -> TcType -> TcType -> TcCoercionP
 mkTcKindCo             :: TcCoercion -> TcCoercionN
 mkTcCoVarCo            :: CoVar -> TcCoercion
+mkTcFamilyTyConAppCo   :: TyCon -> [TcCoercionN] -> TcCoercionN
 
 tcCoercionKind         :: TcCoercion -> Pair TcType
 tcCoercionRole         :: TcCoercion -> Role
@@ -172,6 +174,7 @@ mkTcCoherenceRightCo   = mkCoherenceRightCo
 mkTcPhantomCo          = mkPhantomCo
 mkTcKindCo             = mkKindCo
 mkTcCoVarCo            = mkCoVarCo
+mkTcFamilyTyConAppCo   = mkFamilyTyConAppCo
 
 tcCoercionKind         = coercionKind
 tcCoercionRole         = coercionRole


=====================================
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,
@@ -1746,7 +1746,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


=====================================
ghc.mk
=====================================
@@ -1168,7 +1168,8 @@ SRC_DIST_TESTSUITE_TARBALL        = $(SRC_DIST_ROOT)/$(SRC_DIST_TESTSUITE_NAME).
 # Files to include in source distributions
 #
 SRC_DIST_GHC_DIRS = mk rules docs distrib bindisttest libffi includes \
-    utils docs rts compiler ghc driver libraries libffi-tarballs
+    utils docs rts compiler ghc driver libraries libffi-tarballs \
+		hadrian
 SRC_DIST_GHC_FILES += \
     configure.ac config.guess config.sub configure \
     aclocal.m4 README.md ANNOUNCE HACKING.md INSTALL.md LICENSE Makefile \
@@ -1209,6 +1210,7 @@ sdist-ghc-prep-tree :
 	cd $(SRC_DIST_GHC_DIR) && $(MAKE) distclean
 	$(call removeTrees,$(SRC_DIST_GHC_DIR)/libraries/tarballs/)
 	$(call removeTrees,$(SRC_DIST_GHC_DIR)/libraries/stamp/)
+	$(call removeTrees,$(SRC_DIST_GHC_DIR)/hadrian/_build/ (SRC_DIST_GHC_DIR)/hadrian/dist-newstyle/)
 	$(call removeTrees,$(SRC_DIST_GHC_DIR)/compiler/stage[123])
 	$(call removeFiles,$(SRC_DIST_GHC_DIR)/mk/build.mk)
 	$(call removeFiles,$(SRC_DIST_GHC_DIR)/rts/rts.cabal)


=====================================
testsuite/tests/indexed-types/should_compile/T18809.hs
=====================================
@@ -0,0 +1,33 @@
+{-# LANGUAGE GADTs, TypeFamilies #-}
+
+module T18809 where
+
+-- Ordinary
+data F2 s where
+  MkF2 :: {  foo2 :: Int } -> F2 s
+
+bar2 :: F2 s -> Int -> F2 s
+bar2 z y = z { foo2 = y }
+
+-- GADT
+data F1 s where
+  MkF1 :: {  foo1 :: Int } -> F1 Int
+
+bar1 :: F1 s -> Int -> F1 s
+bar1 z y = z { foo1 = y }
+
+-- Orinary data family
+data family F3 a
+data instance F3 (s,t) where
+  MkF2b :: { foo3 :: Int } -> F3 (s,t)
+
+bar3 :: F3 (s,t) -> Int -> F3 (s,t)
+bar3 z y = z {foo3 = y}
+
+-- GADT + data family
+data family F4 a
+data instance F4 (s,t) where
+  MkF2a :: { foo4 :: Int } -> F4 (Int,t)
+
+bar4 :: F4 (s,t) -> Int -> F4 (s,t)
+bar4 z y = z { foo4 = y}


=====================================
testsuite/tests/indexed-types/should_compile/all.T
=====================================
@@ -296,3 +296,4 @@ test('T17056', normal, compile, [''])
 test('T17405', normal, multimod_compile, ['T17405c', '-v0'])
 test('T17923', normal, compile, [''])
 test('T18065', normal, compile, ['-O'])
+test('T18809', normal, compile, ['-O'])


=====================================
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
=====================================
@@ -336,3 +336,6 @@ test('T18589', normal, compile, ['-dcore-lint -O'])
 
 test('T18747A', normal, compile, [''])
 test('T18747B', normal, compile, [''])
+
+# T18649 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/-/compare/d09e7e41cf79fe981a61eae46a93d8881859ff1f...64ab97bfdae8ca094d677ad27aecf514e7acafd0

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/d09e7e41cf79fe981a61eae46a93d8881859ff1f...64ab97bfdae8ca094d677ad27aecf514e7acafd0
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/20201014/bdb453fb/attachment-0001.html>


More information about the ghc-commits mailing list