[Git][ghc/ghc][wip/T21623] Remove infinite loop in T1946
Simon Peyton Jones (@simonpj)
gitlab at gitlab.haskell.org
Mon Aug 29 23:06:43 UTC 2022
Simon Peyton Jones pushed to branch wip/T21623 at Glasgow Haskell Compiler / GHC
Commits:
8ebd8d3f by Simon Peyton Jones at 2022-08-30T00:06:52+01:00
Remove infinite loop in T1946
See Note [ForAllTy and type equality]
- - - - -
11 changed files:
- compiler/GHC/Core/Reduction.hs
- compiler/GHC/Core/TyCo/Compare.hs
- compiler/GHC/Core/TyCo/Rep.hs
- compiler/GHC/Core/TyCo/Rep.hs-boot
- compiler/GHC/Core/TyCon.hs
- compiler/GHC/Core/Type.hs
- compiler/GHC/Core/Utils.hs
- compiler/GHC/Hs/Syn/Type.hs
- compiler/GHC/Tc/Gen/Foreign.hs
- compiler/GHC/Types/Literal.hs
- compiler/GHC/Types/Name/Occurrence.hs
Changes:
=====================================
compiler/GHC/Core/Reduction.hs
=====================================
@@ -36,7 +36,7 @@ import GHC.Core.Type
import GHC.Data.Pair ( Pair(Pair) )
-import GHC.Types.Var ( setTyVarKind )
+import GHC.Types.Var ( VarBndr(..), setTyVarKind )
import GHC.Types.Var.Env ( mkInScopeSet )
import GHC.Types.Var.Set ( TyCoVarSet )
@@ -375,7 +375,7 @@ mkForAllRedn :: ArgFlag
mkForAllRedn vis tv1 (Reduction h ki') (Reduction co ty)
= mkReduction
(mkForAllCo tv1 h co)
- (mkForAllTy tv2 vis ty)
+ (mkForAllTy (Bndr tv2 vis) ty)
where
tv2 = setTyVarKind tv1 ki'
{-# INLINE mkForAllRedn #-}
=====================================
compiler/GHC/Core/TyCo/Compare.hs
=====================================
@@ -161,7 +161,7 @@ tc_eq_type keep_syns vis_only orig_ty1 orig_ty2
go env (ForAllTy (Bndr tv1 vis1) ty1)
(ForAllTy (Bndr tv2 vis2) ty2)
- = vis1 == vis2
+ = vis1 `eqForAllVis` vis2
&& (vis_only || go env (varType tv1) (varType tv2))
&& go (rnBndr2 env tv1 tv2) ty1 ty2
@@ -218,6 +218,7 @@ tc_eq_type keep_syns vis_only orig_ty1 orig_ty2
-- equates 'Specified' and 'Inferred'. Used for printing.
eqForAllVis :: ArgFlag -> ArgFlag -> Bool
-- See Note [ForAllTy and type equality]
+-- If you change this, see IMPORTANT NOTE in the above Note
eqForAllVis Required Required = True
eqForAllVis (Invisible _) (Invisible _) = True
eqForAllVis _ _ = False
@@ -227,6 +228,7 @@ eqForAllVis _ _ = False
-- equates 'Specified' and 'Inferred'. Used for printing.
cmpForAllVis :: ArgFlag -> ArgFlag -> Ordering
-- See Note [ForAllTy and type equality]
+-- If you change this, see IMPORTANT NOTE in the above Note
cmpForAllVis Required Required = EQ
cmpForAllVis Required (Invisible {}) = LT
cmpForAllVis (Invisible _) Required = GT
@@ -234,7 +236,7 @@ cmpForAllVis (Invisible _) (Invisible _) = EQ
{- Note [ForAllTy and type equality]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When we compare (ForAllTy (Bndr tv1 vis1) ty1)
and (ForAllTy (Bndr tv2 vis2) ty2)
what should we do about `vis1` vs `vis2`.
@@ -266,9 +268,12 @@ programs like the one above. Whether a kind variable binder ends up being
specified or inferred can be somewhat subtle, however, especially for kinds
that aren't explicitly written out in the source code (like in D above).
-For now, we decide to not make the specified/inferred status of an invisible
-type variable binder affect GHC's notion of equality. That is, we have the
-following:
+For now, we decide
+
+ the specified/inferred status of an invisible type variable binder
+ does not affect GHC's notion of equality.
+
+That is, we have the following:
--------------------------------------------------
| Type 1 | Type 2 | Equal? |
@@ -286,6 +291,12 @@ following:
| | forall k -> <...> | Yes |
--------------------------------------------------
+IMPORTANT NOTE: if we want to change this decision, ForAllCo will need to carry
+visiblity (by taking a TyCoVarBinder rathre than a TyCoVar), so that
+coercionLKind/RKind build forall types that match (are equal to) the desired
+ones. Otherwise we get an infinite loop in the solver via canEqCanLHSHetero.
+Examples: T16946, T15079.
+
Historical Note [Typechecker equality vs definitional equality]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
This Note describes some history, in case there are vesitges of this
=====================================
compiler/GHC/Core/TyCo/Rep.hs
=====================================
@@ -1126,8 +1126,8 @@ tcMkScaledFunTys tys ty = foldr mk ty tys
---------------
-- | Like 'mkTyCoForAllTy', but does not check the occurrence of the binder
-- See Note [Unused coercion variable in ForAllTy]
-mkForAllTy :: TyCoVar -> ArgFlag -> Type -> Type
-mkForAllTy tv vis ty = ForAllTy (Bndr tv vis) ty
+mkForAllTy :: TyCoVarBinder -> Type -> Type
+mkForAllTy = ForAllTy
-- | Wraps foralls over the type using the provided 'TyCoVar's from left to right
mkForAllTys :: [TyCoVarBinder] -> Type -> Type
@@ -1139,7 +1139,7 @@ mkInvisForAllTys tyvars = mkForAllTys (tyVarSpecToBinders tyvars)
mkPiTy :: TyCoBinder -> Type -> Type
mkPiTy (Anon af ty1) ty2 = mkScaledFunTy af ty1 ty2
-mkPiTy (Named (Bndr tv vis)) ty = mkForAllTy tv vis ty
+mkPiTy (Named bndr) ty = mkForAllTy bndr ty
mkPiTys :: [TyCoBinder] -> Type -> Type
mkPiTys tbs ty = foldr mkPiTy ty tbs
=====================================
compiler/GHC/Core/TyCo/Rep.hs-boot
=====================================
@@ -3,7 +3,7 @@ module GHC.Core.TyCo.Rep where
import GHC.Utils.Outputable ( Outputable )
import Data.Data ( Data )
-import {-# SOURCE #-} GHC.Types.Var( Var, ArgFlag, AnonArgFlag )
+import {-# SOURCE #-} GHC.Types.Var( Var, VarBndr, ArgFlag, AnonArgFlag )
import {-# SOURCE #-} GHC.Core.TyCon ( TyCon )
data Type
@@ -24,7 +24,7 @@ type ThetaType = [PredType]
type CoercionN = Coercion
type MCoercionN = MCoercion
-mkForAllTy :: Var -> ArgFlag -> Type -> Type
+mkForAllTy :: VarBndr Var ArgFlag -> Type -> Type
mkNakedTyConTy :: TyCon -> Type
mkNakedKindFunTy :: AnonArgFlag -> Type -> Type -> Type
=====================================
compiler/GHC/Core/TyCon.hs
=====================================
@@ -521,7 +521,7 @@ mkTyConKind :: [TyConBinder] -> Kind -> Kind
mkTyConKind bndrs res_kind = foldr mk res_kind bndrs
where
mk :: TyConBinder -> Kind -> Kind
- mk (Bndr tv (NamedTCB vis)) k = mkForAllTy tv vis k
+ mk (Bndr tv (NamedTCB vis)) k = mkForAllTy (Bndr tv vis) k
mk (Bndr tv (AnonTCB af)) k = mkNakedKindFunTy af (varType tv) k
-- mkNakedKindFunTy: see Note [Naked FunTy] in GHC.Builtin.Types
=====================================
compiler/GHC/Core/Type.hs
=====================================
@@ -1659,13 +1659,6 @@ tcSplitTyConApp ty
= tcSplitTyConApp_maybe ty `orElse` pprPanic "tcSplitTyConApp" (ppr ty)
---------------------------
--- | (mkTyConTy tc) returns (TyConApp tc [])
--- but arranges to share that TyConApp among all calls
--- See Note [Sharing nullary TyConApps] in GHC.Core.TyCon
-mkTyConTy :: TyCon -> Type
-mkTyConTy tycon = tyConNullaryTy tycon
-
--------------------
newTyConInstRhs :: TyCon -> [Type] -> Type
-- ^ Unwrap one 'layer' of newtype on a type constructor and its
-- arguments, using an eta-reduced version of the @newtype@ if possible.
=====================================
compiler/GHC/Core/Utils.hs
=====================================
@@ -170,11 +170,11 @@ mkLamTypes :: [Var] -> Type -> Type
mkLamType v body_ty
| isTyVar v
- = mkForAllTy v Inferred body_ty
+ = mkForAllTy (Bndr v Inferred) body_ty
| isCoVar v
, v `elemVarSet` tyCoVarsOfType body_ty
- = mkForAllTy v Required body_ty
+ = mkForAllTy (Bndr v Required) body_ty
| otherwise
= mkFunctionType (varMult v) (varType v) body_ty
=====================================
compiler/GHC/Hs/Syn/Type.hs
=====================================
@@ -24,6 +24,7 @@ import GHC.Core.Type
import GHC.Hs
import GHC.Tc.Types.Evidence
import GHC.Types.Id
+import GHC.Types.Var( VarBndr(..) )
import GHC.Types.SrcLoc
import GHC.Utils.Outputable
import GHC.Utils.Panic
@@ -183,7 +184,7 @@ hsWrapperType wrap ty = prTypeType $ go wrap (ty,[])
go (WpCast co) = liftPRType $ \_ -> coercionRKind co
go (WpEvLam v) = liftPRType $ mkInvisFunTy (idType v)
go (WpEvApp _) = liftPRType $ funResultTy
- go (WpTyLam tv) = liftPRType $ mkForAllTy tv Inferred
+ go (WpTyLam tv) = liftPRType $ mkForAllTy (Bndr tv Inferred)
go (WpTyApp ta) = \(ty,tas) -> (ty, ta:tas)
go (WpLet _) = id
go (WpMultCoercion _) = id
=====================================
compiler/GHC/Tc/Gen/Foreign.hs
=====================================
@@ -44,29 +44,35 @@ import GHC.Tc.Utils.Monad
import GHC.Tc.Gen.HsType
import GHC.Tc.Gen.Expr
import GHC.Tc.Utils.Env
-
+import GHC.Tc.Utils.TcType
import GHC.Tc.Instance.Family
+
import GHC.Core.FamInstEnv
import GHC.Core.Coercion
import GHC.Core.Reduction
import GHC.Core.Type
import GHC.Core.Multiplicity
+import GHC.Core.DataCon
+import GHC.Core.TyCon
+import GHC.Core.TyCon.RecWalk
+
import GHC.Types.ForeignCall
-import GHC.Utils.Error
import GHC.Types.Id
import GHC.Types.Name
import GHC.Types.Name.Reader
-import GHC.Core.DataCon
-import GHC.Core.TyCon
-import GHC.Core.TyCon.RecWalk
-import GHC.Tc.Utils.TcType
+import GHC.Types.SrcLoc
+
import GHC.Builtin.Names
+import GHC.Builtin.Types.Prim( isArrowTyCon )
+
import GHC.Driver.Session
import GHC.Driver.Backend
+
+import GHC.Utils.Error
import GHC.Utils.Outputable as Outputable
import GHC.Utils.Panic
import GHC.Platform
-import GHC.Types.SrcLoc
+
import GHC.Data.Bag
import GHC.Driver.Hooks
import qualified GHC.LanguageExtensions as LangExt
=====================================
compiler/GHC/Types/Literal.hs
=====================================
@@ -853,7 +853,7 @@ literalType (LitNumber lt _) = case lt of
-- LitRubbish: see Note [Rubbish literals]
literalType (LitRubbish torc rep)
- = mkForAllTy a Inferred (mkTyVarTy a)
+ = mkForAllTy (Bndr a Inferred) (mkTyVarTy a)
where
a = mkTemplateKindVar kind
kind = case torc of
=====================================
compiler/GHC/Types/Name/Occurrence.hs
=====================================
@@ -791,7 +791,6 @@ after we allocate a new one.
Note [Tidying multiple names at once]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-
Consider
> :t (id,id,id)
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/8ebd8d3f9ac254a49244290e0c767c9ab8892b7c
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/8ebd8d3f9ac254a49244290e0c767c9ab8892b7c
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/20220829/401b2583/attachment-0001.html>
More information about the ghc-commits
mailing list