[Git][ghc/ghc][master] Use checkTyEqRhs to make types concrete
Marge Bot (@marge-bot)
gitlab at gitlab.haskell.org
Fri Jan 17 16:18:04 UTC 2025
Marge Bot pushed to branch master at Glasgow Haskell Compiler / GHC
Commits:
87e82e2e by sheaf at 2025-01-16T14:51:45+01:00
Use checkTyEqRhs to make types concrete
This commit refactors makeTypeConcrete to call checkTyEqRhs with
the appropriate parameters. This avoids duplicating subtle logic
in two places in the compiler.
Changes:
1. Refactor of 'TyEqFlags'. Now 'TyEqFlags' stores a 'TEFTask', which
is a description of which of the following checks we want to
perform in 'checkTyEqRhs':
- occurs check
- level check
- concreteness check
In the process, the 'AreUnifying' datatype has been removed, as it
is no longer needed.
2. Refactor of 'checkTyVar':
a. Make use of the new 'TEFTask' data type to decide which checks
to perform.
In particular, this ensures that we perform **both** a
concreteness check and a level check when both are required;
previously we only did a concreteness check (that was a bug!).
b. Recursively call 'checkTyVar' on the kind of unfilled
metavariables. This deals with a bug in which we failed to
uphold the invariant that the kind of a concrete type must
itself be concrete. See test cases T23051, T23176.
3. Re-write of 'makeTypeConcrete', which now simply calls
'checkTyEqRhs' with appropriate 'TyEqFlags'/'TEFTask'.
This gets rid of code duplication and risk for the two code paths
going out-of-sync.
Fixes #25616. See also #23883.
- - - - -
17 changed files:
- compiler/GHC/Core/Type.hs
- compiler/GHC/Tc/Errors.hs
- compiler/GHC/Tc/Gen/App.hs
- compiler/GHC/Tc/Solver/Default.hs
- compiler/GHC/Tc/Solver/Monad.hs
- compiler/GHC/Tc/Types/Constraint.hs
- compiler/GHC/Tc/Utils/Concrete.hs
- compiler/GHC/Tc/Utils/TcMType.hs
- compiler/GHC/Tc/Utils/TcType.hs
- compiler/GHC/Tc/Utils/Unify.hs
- compiler/GHC/Tc/Utils/Unify.hs-boot
- hie.yaml
- testsuite/tests/rep-poly/RepPolyInferPatBind.stderr
- testsuite/tests/rep-poly/RepPolyInferPatSyn.stderr
- testsuite/tests/rep-poly/RepPolyTuple3.stderr
- testsuite/tests/rep-poly/T23153.stderr
- testsuite/tests/rep-poly/T23154.stderr
Changes:
=====================================
compiler/GHC/Core/Type.hs
=====================================
@@ -235,7 +235,8 @@ module GHC.Core.Type (
-- * Kinds
isTYPEorCONSTRAINT,
- isConcreteType, isFixedRuntimeRepKind,
+ isConcreteType,
+ isFixedRuntimeRepKind
) where
import GHC.Prelude
@@ -2869,12 +2870,14 @@ isFixedRuntimeRepKind k
isConcreteType :: Type -> Bool
isConcreteType = isConcreteTypeWith emptyVarSet
-isConcreteTypeWith :: TyVarSet -> Type -> Bool
+-- | Like 'isConcreteType', but allows passing in a set of 'TyVar's that
+-- should be considered concrete.
+--
-- See Note [Concrete types] in GHC.Tc.Utils.Concrete.
--- For this "With" version we pass in a set of TyVars to be considered
--- concrete. This supports mkSynonymTyCon, which needs to test the RHS
--- for concreteness, under the assumption that the binders are instantiated
--- to concrete types
+isConcreteTypeWith :: TyVarSet -> Type -> Bool
+-- This version, with a 'TyVarSet' argument, supports 'mkSynonymTyCon',
+-- which needs to test the RHS for concreteness, under the assumption that
+-- the binders are instantiated to concrete types
isConcreteTypeWith conc_tvs = go
where
go (TyVarTy tv) = isConcreteTyVar tv || tv `elemVarSet` conc_tvs
@@ -2888,6 +2891,7 @@ isConcreteTypeWith conc_tvs = go
go CastTy{} = False
go CoercionTy{} = False
+ go_tc :: TyCon -> [Type] -> Bool
go_tc tc tys
| isForgetfulSynTyCon tc -- E.g. type S a = Int
-- Then (S x) is concrete even if x isn't
@@ -2903,7 +2907,6 @@ isConcreteTypeWith conc_tvs = go
| otherwise -- E.g. type families
= False
-
{-
%************************************************************************
%* *
=====================================
compiler/GHC/Tc/Errors.hs
=====================================
@@ -1048,8 +1048,7 @@ reportNotConcreteErrs ctxt errs@(err0:_)
| frr_errs <- go frr_errs errs
= case err of
NCE_FRR
- { nce_frr_origin = frr_orig
- , nce_reasons = _not_conc } ->
+ { nce_frr_origin = frr_orig } ->
FRR_Info
{ frr_info_origin = frr_orig
, frr_info_not_concrete = Nothing }
=====================================
compiler/GHC/Tc/Gen/App.hs
=====================================
@@ -1202,8 +1202,7 @@ tc_inst_forall_arg conc_tvs (tvb, inner_ty) hs_ty
->
-- Example: user wrote e.g. (#,#) @(F Bool) for a type family F.
-- Emit [W] F Bool ~ kappa[conc] and pretend the user wrote (#,#) @kappa.
- do { mco <- unifyConcrete (occNameFS $ getOccName $ tv_nm) conc ty_arg0
- ; return $ case mco of { MRefl -> ty_arg0; MCo co -> coercionRKind co } }
+ coercionRKind <$> unifyConcrete (occNameFS $ getOccName $ tv_nm) conc ty_arg0
; let fun_ty = mkForAllTy tvb inner_ty
in_scope = mkInScopeSet (tyCoVarsOfTypes [fun_ty, ty_arg])
=====================================
compiler/GHC/Tc/Solver/Default.hs
=====================================
@@ -440,7 +440,7 @@ defaultEquality ct
where
try_default_tv lhs_tv rhs_ty
- | MetaTv { mtv_info = info, mtv_tclvl = lvl } <- tcTyVarDetails lhs_tv
+ | MetaTv { mtv_info = info } <- tcTyVarDetails lhs_tv
, tyVarKind lhs_tv `tcEqType` typeKind rhs_ty
, checkTopShape info rhs_ty
-- Do not test for touchability of lhs_tv; that is the whole point!
@@ -449,14 +449,13 @@ defaultEquality ct
-- checkTyEqRhs: check that we can in fact unify lhs_tv := rhs_ty
-- See Note [Defaulting equalities]
- -- LC_Promote: promote deeper unification variables (DE4)
- -- LC_Promote True: ...including under type families (DE5)
- ; let flags :: TyEqFlags ()
- flags = TEF { tef_foralls = False
- , tef_fam_app = TEFA_Recurse
- , tef_lhs = TyVarLHS lhs_tv
- , tef_unifying = Unifying info lvl (LC_Promote True)
- , tef_occurs = cteInsolubleOccurs }
+ ; let task :: TEFTask
+ task = unifyingLHSMetaTyVar_TEFTask lhs_tv (LC_Promote True)
+ -- LC_Promote: promote deeper unification variables (DE4)
+ -- LC_Promote True: ...including under type families (DE5)
+ flags :: TyEqFlags ()
+ flags = TEF { tef_task = task
+ , tef_fam_app = TEFA_Recurse }
; res :: PuResult () Reduction <- wrapTcS (checkTyEqRhs flags rhs_ty)
; case res of
=====================================
compiler/GHC/Tc/Solver/Monad.hs
=====================================
@@ -201,6 +201,7 @@ import GHC.Exts (oneShot)
import Control.Monad
import Data.IORef
import Data.List ( mapAccumL )
+import Data.Maybe ( isJust )
import Data.Foldable
import qualified Data.Semigroup as S
import GHC.Types.SrcLoc
@@ -2122,7 +2123,7 @@ checkTouchableTyVarEq ev lhs_tv rhs
_ -> pprPanic "checkTouchableTyVarEq" (ppr lhs_tv)
-- lhs_tv should be a meta-tyvar
- is_concrete_lhs_tv = isConcreteInfo lhs_tv_info
+ is_concrete_lhs_tv = isJust $ concreteInfo_maybe lhs_tv_info
check_rhs rhs
-- Crucial special case for alpha ~ F tys
@@ -2134,11 +2135,9 @@ checkTouchableTyVarEq ev lhs_tv rhs
| otherwise
= checkTyEqRhs flags rhs
- flags = TEF { tef_foralls = False -- isRuntimeUnkSkol lhs_tv
- , tef_fam_app = mkTEFA_Break ev NomEq break_wanted
- , tef_unifying = Unifying lhs_tv_info lhs_tv_lvl (LC_Promote False)
- , tef_lhs = TyVarLHS lhs_tv
- , tef_occurs = cteInsolubleOccurs }
+ flags = TEF { tef_task = unifyingLHSMetaTyVar_TEFTask lhs_tv (LC_Promote False)
+ , tef_fam_app = mkTEFA_Break ev NomEq break_wanted
+ }
arg_flags = famAppArgFlags flags
@@ -2147,7 +2146,8 @@ checkTouchableTyVarEq ev lhs_tv rhs
-- Occurs check or skolem escape; so flatten
= do { let fam_app_kind = typeKind fam_app
; reason <- checkPromoteFreeVars cteInsolubleOccurs
- lhs_tv lhs_tv_lvl (tyCoVarsOfType fam_app_kind)
+ (tyVarName lhs_tv) lhs_tv_lvl
+ (tyCoVarsOfType fam_app_kind)
; if not (cterHasNoProblem reason) -- Failed to promote free vars
then failCheckWith reason
else
@@ -2210,19 +2210,15 @@ checkTypeEq ev eq_rel lhs rhs
arg_flags = famAppArgFlags given_flags
given_flags :: TyEqFlags (TcTyVar,TcType)
- given_flags = TEF { tef_lhs = lhs
- , tef_foralls = False
- , tef_unifying = NotUnifying
- , tef_fam_app = mkTEFA_Break ev eq_rel break_given
- , tef_occurs = occ_prob }
+ given_flags = TEF { tef_task = notUnifying_TEFTask occ_prob lhs
+ , tef_fam_app = mkTEFA_Break ev eq_rel break_given
+ }
-- TEFA_Break used for: [G] a ~ Maybe (F a)
-- or [W] F a ~ Maybe (F a)
- wanted_flags = TEF { tef_lhs = lhs
- , tef_foralls = False
- , tef_unifying = NotUnifying
- , tef_fam_app = TEFA_Recurse
- , tef_occurs = occ_prob }
+ wanted_flags = TEF { tef_task = notUnifying_TEFTask occ_prob lhs
+ , tef_fam_app = TEFA_Recurse
+ }
-- TEFA_Recurse: see Note [Don't cycle-break Wanteds when not unifying]
-- occ_prob: see Note [Occurs check and representational equality]
@@ -2289,7 +2285,7 @@ where both sides are TyFamLHSs. We don't want to flatten that RHS to
Instead we'd like to say "occurs-check" and swap LHS and RHS, which yields a
canonical constraint
[G] G (...(F ty)...) ~ F ty
-That tents to rewrite a big type to smaller one. This happens in T15703,
+That tends to rewrite a big type to smaller one. This happens in T15703,
where we had:
[G] Pure g ~ From1 (To1 (Pure g))
Making a loop breaker and rewriting left to right just makes much bigger
=====================================
compiler/GHC/Tc/Types/Constraint.hs
=====================================
@@ -52,7 +52,6 @@ module GHC.Tc.Types.Constraint (
Hole(..), HoleSort(..), isOutOfScopeHole,
DelayedError(..), NotConcreteError(..),
- NotConcreteReason(..),
WantedConstraints(..), insolubleWC, emptyWC, isEmptyWC,
isSolvedWC, andWC, unionsWC, mkSimpleWC, mkImplicWC,
@@ -132,7 +131,6 @@ import Data.Coerce
import qualified Data.Semigroup as S
import Control.Monad ( msum, when )
import Data.Maybe ( mapMaybe, isJust )
-import Data.List.NonEmpty ( NonEmpty )
-- these are for CheckTyEqResult
import Data.Word ( Word8 )
@@ -435,30 +433,8 @@ data NotConcreteError
-- ^ Where did this check take place?
, nce_frr_origin :: FixedRuntimeRepOrigin
-- ^ Which representation-polymorphism check did we perform?
- , nce_reasons :: NonEmpty NotConcreteReason
- -- ^ Why did the check fail?
}
--- | Why did we decide that a type was not concrete?
-data NotConcreteReason
- -- | The type contains a 'TyConApp' of a non-concrete 'TyCon'.
- --
- -- See Note [Concrete types] in GHC.Tc.Utils.Concrete.
- = NonConcreteTyCon TyCon [TcType]
-
- -- | The type contains a type variable that could not be made
- -- concrete (e.g. a skolem type variable).
- | NonConcretisableTyVar TyVar
-
- -- | The type contains a cast.
- | ContainsCast TcType TcCoercionN
-
- -- | The type contains a forall.
- | ContainsForall ForAllTyBinder TcType
-
- -- | The type contains a 'CoercionTy'.
- | ContainsCoercionTy TcCoercion
-
instance Outputable NotConcreteError where
ppr (NCE_FRR { nce_frr_origin = frr_orig })
= text "NCE_FRR" <+> parens (ppr (frr_type frr_orig))
=====================================
compiler/GHC/Tc/Utils/Concrete.hs
=====================================
@@ -19,39 +19,35 @@ module GHC.Tc.Utils.Concrete
import GHC.Prelude
import GHC.Builtin.Names ( unsafeCoercePrimName )
-import GHC.Builtin.Types ( liftedTypeKindTyCon, unliftedTypeKindTyCon )
+import GHC.Builtin.Types
-import GHC.Core.Coercion ( coToMCo, mkCastTyMCo
- , mkGReflRightMCo, mkNomReflCo )
-import GHC.Core.TyCo.Rep ( Type(..), MCoercion(..) )
-import GHC.Core.TyCon ( isConcreteTyCon )
-import GHC.Core.Type ( isConcreteType, typeKind, mkFunTy)
+import GHC.Core.Coercion
+import GHC.Core.TyCo.Rep
+import GHC.Core.Type
-import GHC.Tc.Types.Constraint ( NotConcreteError(..), NotConcreteReason(..) )
-import GHC.Tc.Types.Evidence ( Role(..), TcCoercionN, TcMCoercionN )
+import GHC.Data.Bag
+
+import GHC.Tc.Types.Constraint
+import GHC.Tc.Types.Evidence
import GHC.Tc.Types.Origin
import GHC.Tc.Utils.Monad
import GHC.Tc.Utils.TcType
-import GHC.Tc.Utils.TcMType
+import {-# SOURCE #-} GHC.Tc.Utils.Unify
import GHC.Types.Basic ( TypeOrKind(KindLevel) )
import GHC.Types.Id
import GHC.Types.Id.Info
-import GHC.Types.Name
import GHC.Types.Name.Env
-import GHC.Types.Var ( tyVarKind, tyVarName )
+import GHC.Types.Var
import GHC.Utils.Misc ( HasDebugCallStack )
import GHC.Utils.Outputable
+import GHC.Utils.Panic
import GHC.Data.FastString ( FastString, fsLit )
-
import Control.Monad ( void )
import Data.Functor ( ($>) )
-import Data.List.NonEmpty ( NonEmpty((:|)) )
-import Control.Monad.Trans.Class ( lift )
-import Control.Monad.Trans.Writer.CPS ( WriterT, runWriterT, tell )
{- Note [Concrete overview]
~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -221,7 +217,6 @@ other type variables, a 'ConcreteTv' type variable is a type variable which can
only be unified with a concrete type (in the sense of Note [Concrete types]).
INVARIANT: the kind of a concrete metavariable is concrete.
-
This invariant is upheld at the time of creation of a new concrete metavariable.
Concrete metavariables are useful for representation-polymorphism checks:
@@ -632,7 +627,7 @@ hasFixedRuntimeRep :: HasDebugCallStack
-- That is, @ty'@ has a syntactically fixed RuntimeRep
-- in the sense of Note [Fixed RuntimeRep].
hasFixedRuntimeRep frr_ctxt ty =
- checkFRR_with (unifyConcrete (fsLit "cx") . ConcreteFRR) frr_ctxt ty
+ checkFRR_with (fmap (fmap coToMCo) . unifyConcrete_kind (fsLit "cx") . ConcreteFRR) frr_ctxt ty
-- | Like 'hasFixedRuntimeRep', but we perform an eager syntactic check.
--
@@ -700,226 +695,86 @@ checkFRR_with check_kind frr_ctxt ty
frr_orig :: FixedRuntimeRepOrigin
frr_orig = FixedRuntimeRepOrigin { frr_type = ty, frr_context = frr_ctxt }
--- | Ensure that the given type @ty@ can unify with a concrete type,
+-- | Ensure that the given kind @ki@ can unify with a concrete type,
-- in the sense of Note [Concrete types].
--
--- Returns a coercion @co :: ty ~# conc_ty@, where @conc_ty@ is
+-- Returns a coercion @co :: ki ~# conc_ki@, where @conc_ki@ is
-- concrete.
--
--- If the type is already syntactically concrete, this
+-- If the kind is already syntactically concrete, this
-- immediately returns a reflexive coercion. Otherwise,
-- it creates a new concrete metavariable @concrete_tv@
--- and emits an equality constraint @ty ~# concrete_tv@,
+-- and emits an equality constraint @ki ~# concrete_tv@,
-- to be handled by the constraint solver.
--
+-- Precondition: @ki@ must be of the form @TYPE rep@ or @CONSTRAINT rep at .
+unifyConcrete_kind :: HasDebugCallStack
+ => FastString -- ^ name to use when creating concrete metavariables
+ -> ConcreteTvOrigin
+ -> TcKind
+ -> TcM TcCoercionN
+unifyConcrete_kind occ_fs conc_orig ki
+ | Just (torc, rep) <- sORTKind_maybe ki
+ = do { let tc = case torc of
+ TypeLike -> tYPETyCon
+ ConstraintLike -> cONSTRAINTTyCon
+ ; rep_co <- unifyConcrete occ_fs conc_orig rep
+ ; return $ mkTyConAppCo Nominal tc [rep_co] }
+ | otherwise
+ = pprPanic "unifyConcrete_kind: kind is not of the form 'TYPE rep' or 'CONSTRAINT rep'" $
+ ppr ki <+> dcolon <+> ppr (typeKind ki)
+
+
+-- | Ensure the given type can be unified with
+-- a concrete type, in the sense of Note [Concrete types].
+--
+-- Returns a coercion @co :: ty ~# conc_ty@, where @conc_ty@ is
+-- concrete.
+--
+-- If the type is already syntactically concrete, this
+-- immediately returns a reflexive coercion.
+-- Otherwise, it will create new concrete metavariables and emit
+-- new Wanted equality constraints, to be handled by the constraint solver.
+--
-- Invariant: the kind of the supplied type must be concrete.
--
-- We assume the provided type is already at the kind-level
-- (this only matters for error messages).
-unifyConcrete :: HasDebugCallStack
- => FastString -> ConcreteTvOrigin -> TcType -> TcM TcMCoercionN
+unifyConcrete :: FastString -> ConcreteTvOrigin -> TcType -> TcM TcCoercionN
unifyConcrete occ_fs conc_orig ty
- = do { (ty, errs) <- makeTypeConcrete conc_orig ty
- ; case errs of
- -- We were able to make the type fully concrete.
- { [] -> return MRefl
- -- The type could not be made concrete; perhaps it contains
- -- a skolem type variable, a type family application, ...
- --
- -- Create a new ConcreteTv metavariable @concrete_tv@
- -- and unify @ty ~# concrete_tv at .
- ; _ ->
- do { conc_tv <- newConcreteTyVar conc_orig occ_fs ki
- -- NB: newConcreteTyVar asserts that 'ki' is concrete.
- ; coToMCo <$> emitWantedEq orig KindLevel Nominal ty (mkTyVarTy conc_tv) } } }
- where
- ki :: TcKind
- ki = typeKind ty
- orig :: CtOrigin
- orig = case conc_orig of
- ConcreteFRR frr_orig -> FRROrigin frr_orig
+ = do { (co, cts) <- makeTypeConcrete occ_fs conc_orig ty
+ ; emitSimples cts
+ ; return co }
--- | Ensure that the given type is concrete.
+-- | Ensure that the given kind @ki@ is concrete.
--
-- This is an eager syntactic check, and never defers
--- any work to the constraint solver.
---
--- Invariant: the kind of the supplied type must be concrete.
--- Invariant: the output type is equal to the input type,
--- up to zonking.
+-- any work to the constraint solver. However,
+-- it may perform unification.
--
--- We assume the provided type is already at the kind-level
--- (this only matters for error messages).
+-- Invariant: the output type is equal to the input type, up to zonking.
ensureConcrete :: HasDebugCallStack
=> FixedRuntimeRepOrigin
- -> TcType
- -> TcM TcType
-ensureConcrete frr_orig ty
- = do { traceTc "ensureConcrete {" (ppr frr_orig $$ ppr ty)
- ; (ty', errs) <- makeTypeConcrete conc_orig ty
- ; case errs of
- { err:errs ->
- do { traceTc "ensureConcrete } failure" $
- vcat [ text "ty:" <+> ppr ty
- , text "ty':" <+> ppr ty' ]
+ -> TcKind
+ -> TcM TcKind
+ensureConcrete frr_orig ki
+ = do { (co, cts) <- makeTypeConcrete (fsLit "cx") conc_orig ki
+ ; let trace_msg = vcat [ text "ty: " <+> ppr ki
+ , text "co:" <+> ppr co ]
+ ; if isEmptyBag cts
+ then traceTc "ensureConcrete } success" trace_msg
+ else do { traceTc "ensureConcrete } failure" trace_msg
; loc <- getCtLocM (FRROrigin frr_orig) (Just KindLevel)
; emitNotConcreteError $
NCE_FRR
{ nce_loc = loc
- , nce_frr_origin = frr_orig
- , nce_reasons = err :| errs }
- }
- ; [] ->
- traceTc "ensureConcrete } success" $
- vcat [ text "ty: " <+> ppr ty
- , text "ty':" <+> ppr ty' ] }
- ; return ty' }
+ , nce_frr_origin = frr_orig }
+ }
+ ; return $ coercionRKind co }
where
conc_orig :: ConcreteTvOrigin
conc_orig = ConcreteFRR frr_orig
-{-***********************************************************************
-%* *
- Making a type concrete
-%* *
-%************************************************************************
-
-Note [Unifying concrete metavariables]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Unifying concrete metavariables (as defined in Note [ConcreteTv]) is not
-an all-or-nothing affair as it is for other sorts of metavariables.
-
-Consider the following unification problem in which all metavariables
-are unfilled (and ignoring any TcLevel considerations):
-
- alpha[conc] ~# TYPE (TupleRep '[ beta[conc], IntRep, gamma[tau] ])
-
-We can't immediately unify `alpha` with the RHS, because the RHS is not
-a concrete type (in the sense of Note [Concrete types]). Instead, we
-proceed as follows:
-
- - create a fresh concrete metavariable variable `gamma'[conc]`,
- - write gamma[tau] := gamma'[conc],
- - write alpha[conc] := TYPE (TupleRep '[ beta[conc], IntRep, gamma'[conc] ]).
-
-Thus, in general, to unify `alpha[conc] ~# rhs`, we first try to turn
-`rhs` into a concrete type (see the 'makeTypeConcrete' function).
-If this succeeds, resulting in a concrete type `rhs'`, we simply fill
-`alpha[conc] := rhs'`. If it fails, then syntactic unification fails.
-
-Example 1:
-
- alpha[conc] ~# TYPE (TupleRep '[ beta[conc], IntRep, gamma[tau] ])
-
- We proceed by filling metavariables:
-
- gamma[tau] := gamma[conc]
- alpha[conc] := TYPE (TupleRep '[ beta[conc], IntRep, gamma[conc] ])
-
- This successfully unifies alpha.
-
-Example 2:
-
- For a type family `F :: Type -> Type`:
-
- delta[conc] ~# TYPE (SumRep '[ zeta[tau], a[sk], F omega[tau] ])
-
- We write zeta[tau] := zeta[conc], and then fail, providing the following
- two reasons:
-
- - `a[sk]` is not a concrete type variable, so the overall type
- cannot be concrete
- - `F` is not a concrete type constructor, in the sense of
- Note [Concrete types]. So we keep it as is; in particular,
- we /should not/ try to make its argument `omega[tau]` into
- a ConcreteTv.
-
- Note that making zeta concrete allows us to propagate information.
- For example, after more typechecking, we might try to unify
- `zeta ~# rr[sk]`. If we made zeta a ConcreteTv, we will report
- this unsolved equality using the 'ConcreteTvOrigin' stored in zeta[conc].
- This allows us to report ALL the problems in a representation-polymorphism
- check (instead of only a non-empty subset).
--}
-
--- | Try to turn the provided type into a concrete type, by ensuring
--- unfilled metavariables are appropriately marked as concrete.
---
--- Returns a zonked type which is "as concrete as possible", and
--- a list of problems encountered when trying to make it concrete.
---
--- INVARIANT: the returned type is equal to the input type, up to zonking.
--- INVARIANT: if this function returns an empty list of 'NotConcreteReasons',
--- then the returned type is concrete, in the sense of Note [Concrete types].
-makeTypeConcrete :: ConcreteTvOrigin -> TcType -> TcM (TcType, [NotConcreteReason])
--- TODO: it could be worthwhile to return enough information to continue solving.
--- Consider unifying `alpha[conc] ~# TupleRep '[ beta[tau], F Int ]` for
--- a type family 'F'.
--- This function will concretise `beta[tau] := beta[conc]` and return
--- that `TupleRep '[ beta[conc], F Int ]` is not concrete because of the
--- type family application `F Int`. But we could decompose by setting
--- alpha := TupleRep '[ beta, gamma[conc] ] and emitting `[W] gamma[conc] ~ F Int`.
-makeTypeConcrete conc_orig ty =
- do { res@(ty', _) <- runWriterT $ go ty
- ; traceTc "makeTypeConcrete" $
- vcat [ text "ty:" <+> ppr ty
- , text "ty':" <+> ppr ty' ]
- ; return res }
- where
- go :: TcType -> WriterT [NotConcreteReason] TcM TcType
- go ty
- | Just ty <- coreView ty
- = go ty
- | isConcreteType ty
- = pure ty
- go ty@(TyVarTy tv) -- not a ConcreteTv (already handled above)
- = do { mb_filled <- lift $ isFilledMetaTyVar_maybe tv
- ; case mb_filled of
- { Just ty -> go ty
- ; Nothing
- | isMetaTyVar tv
- , TauTv <- metaTyVarInfo tv
- -> -- Change the MetaInfo to ConcreteTv, but retain the TcLevel
- do { kind <- go (tyVarKind tv)
- ; let occ_fs = occNameFS (getOccName tv)
- -- occ_fs: preserve the occurrence name of the original tyvar
- -- This helps in error messages
- ; lift $
- do { conc_tv <- setTcLevel (tcTyVarLevel tv) $
- newConcreteTyVar conc_orig occ_fs kind
- ; let conc_ty = mkTyVarTy conc_tv
- ; liftZonkM $ writeMetaTyVar tv conc_ty
- ; return conc_ty } }
- | otherwise
- -- Don't attempt to make other type variables concrete
- -- (e.g. SkolemTv, TyVarTv, CycleBreakerTv, RuntimeUnkTv).
- -> bale_out ty (NonConcretisableTyVar tv) } }
- go ty@(TyConApp tc tys)
- | isConcreteTyCon tc
- = mkTyConApp tc <$> mapM go tys
- | otherwise
- = bale_out ty (NonConcreteTyCon tc tys)
- go (FunTy af w ty1 ty2)
- = do { w <- go w
- ; ty1 <- go ty1
- ; ty2 <- go ty2
- ; return $ mkFunTy af w ty1 ty2 }
- go (AppTy ty1 ty2)
- = do { ty1 <- go ty1
- ; ty2 <- go ty2
- ; return $ mkAppTy ty1 ty2 }
- go ty@(LitTy {})
- = return ty
- go ty@(CastTy cast_ty kco)
- = bale_out ty (ContainsCast cast_ty kco)
- go ty@(ForAllTy tcv body)
- = bale_out ty (ContainsForall tcv body)
- go ty@(CoercionTy co)
- = bale_out ty (ContainsCoercionTy co)
-
- bale_out :: TcType -> NotConcreteReason -> WriterT [NotConcreteReason] TcM TcType
- bale_out ty reason = do { tell [reason]; return ty }
-
{-***********************************************************************
%* *
Concrete type variables of Ids
=====================================
compiler/GHC/Tc/Utils/TcMType.hs
=====================================
@@ -755,7 +755,7 @@ newNamedAnonMetaTyVar tyvar_name meta_info kind
= do { name <- newMetaTyVarName tyvar_name
; details <- newMetaDetails meta_info
; let tyvar = mkTcTyVar name kind details
- ; traceTc "newAnonMetaTyVar" (ppr tyvar)
+ ; traceTc "newAnonMetaTyVar" (ppr tyvar <+> dcolon <+> ppr kind)
; return tyvar }
-- makes a new skolem tv
=====================================
compiler/GHC/Tc/Utils/TcType.hs
=====================================
@@ -53,7 +53,7 @@ module GHC.Tc.Utils.TcType (
isImmutableTyVar, isSkolemTyVar, isMetaTyVar, isMetaTyVarTy, isTyVarTy,
tcIsTcTyVar, isTyVarTyVar, isOverlappableTyVar, isTyConableTyVar,
ConcreteTvOrigin(..), isConcreteTyVar_maybe, isConcreteTyVar,
- isConcreteTyVarTy, isConcreteTyVarTy_maybe, isConcreteInfo,
+ isConcreteTyVarTy, isConcreteTyVarTy_maybe, concreteInfo_maybe,
ConcreteTyVars, noConcreteTyVars,
isAmbiguousTyVar, isCycleBreakerTyVar, metaTyVarRef, metaTyVarInfo,
isFlexi, isIndirect, isRuntimeUnkSkol,
@@ -1266,9 +1266,9 @@ isConcreteTyVar_maybe tv
| otherwise
= Nothing
-isConcreteInfo :: MetaInfo -> Bool
-isConcreteInfo (ConcreteTv {}) = True
-isConcreteInfo _ = False
+concreteInfo_maybe :: MetaInfo -> Maybe ConcreteTvOrigin
+concreteInfo_maybe (ConcreteTv conc_orig) = Just conc_orig
+concreteInfo_maybe _ = Nothing
-- | Is this type variable a concrete type variable, i.e.
-- it is a metavariable with 'ConcreteTv' 'MetaInfo'?
=====================================
compiler/GHC/Tc/Utils/Unify.hs
=====================================
@@ -1,8 +1,13 @@
+{-# LANGUAGE DeriveTraversable #-}
+{-# LANGUAGE DerivingStrategies #-}
+{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE RecursiveDo #-}
{-# LANGUAGE MultiWayIf #-}
{-# LANGUAGE RecordWildCards #-}
+{-# LANGUAGE TypeApplications #-}
+
{-
(c) The University of Glasgow 2006
@@ -28,6 +33,7 @@ module GHC.Tc.Utils.Unify (
swapOverTyVars, touchabilityAndShapeTest, checkTopShape, lhsPriority,
UnifyEnv(..), updUEnvLoc, setUEnvRole,
uType,
+ makeTypeConcrete,
--------------------------------
-- Holes
@@ -41,8 +47,11 @@ module GHC.Tc.Utils.Unify (
checkTyEqRhs, recurseIntoTyConApp,
PuResult(..), failCheckWith, okCheckRefl, mapCheck,
- TyEqFlags(..), TyEqFamApp(..), AreUnifying(..), LevelCheck(..), FamAppBreaker,
+ TyEqFlags(..), TEFTask(..),
+ notUnifying_TEFTask, unifyingLHSMetaTyVar_TEFTask,
+ LevelCheck(..), TyEqFamApp(..), FamAppBreaker,
famAppArgFlags, checkPromoteFreeVars,
+
simpleUnifyCheck, UnifyCheckCaller(..),
fillInferResult,
@@ -54,7 +63,7 @@ import GHC.Hs
import GHC.Tc.Errors.Types ( ErrCtxtMsg(..) )
import GHC.Tc.Errors.Ppr ( pprErrCtxtMsg )
-import GHC.Tc.Utils.Concrete ( hasFixedRuntimeRep, hasFixedRuntimeRep_syntactic )
+import GHC.Tc.Utils.Concrete
import GHC.Tc.Utils.Env
import GHC.Tc.Utils.Instantiate
import GHC.Tc.Utils.Monad
@@ -94,11 +103,13 @@ import GHC.Utils.Panic
import GHC.Driver.DynFlags
import GHC.Data.Bag
-import GHC.Data.FastString( fsLit )
+import GHC.Data.FastString
import Control.Monad
+import Data.Maybe (maybeToList, isJust)
import Data.Monoid as DM ( Any(..) )
import qualified Data.Semigroup as S ( (<>) )
+import Data.Traversable (for)
{- *********************************************************************
* *
@@ -2927,7 +2938,7 @@ simpleUnifyCheck caller lhs_tv rhs
= go rhs
where
- !(occ_in_ty, occ_in_co) = mkOccFolders lhs_tv
+ !(occ_in_ty, occ_in_co) = mkOccFolders (tyVarName lhs_tv)
lhs_tv_lvl = tcTyVarLevel lhs_tv
lhs_tv_is_concrete = isConcreteTyVar lhs_tv
@@ -2974,7 +2985,7 @@ simpleUnifyCheck caller lhs_tv rhs
go (LitTy {}) = True
-mkOccFolders :: TcTyVar -> (TcType -> Bool, TcCoercion -> Bool)
+mkOccFolders :: Name -> (TcType -> Bool, TcCoercion -> Bool)
-- These functions return True
-- * if lhs_tv occurs (incl deeply, in the kind of variable)
-- * if there is a coercion hole
@@ -2987,7 +2998,7 @@ mkOccFolders lhs_tv = (getAny . check_ty, getAny . check_co)
, tcf_hole = do_hole
, tcf_tycobinder = do_bndr }
- do_tcv is v = Any (not (v `elemVarSet` is) && v == lhs_tv)
+ do_tcv is v = Any (not (v `elemVarSet` is) && tyVarName v == lhs_tv)
`mappend` check_ty (varType v)
do_bndr is tcv _faf = extendVarSet is tcv
@@ -3058,10 +3069,7 @@ reductionCoercion is Refl. See `canEqCanLHSFinish_no_unification`.
data PuResult a b = PuFail CheckTyEqResult
| PuOK (Bag a) b
-
-instance Functor (PuResult a) where
- fmap _ (PuFail prob) = PuFail prob
- fmap f (PuOK cts x) = PuOK cts (f x)
+ deriving stock (Functor, Foldable, Traversable)
instance Applicative (PuResult a) where
pure x = PuOK emptyBag x
@@ -3100,82 +3108,192 @@ mapCheck f xs
-- | Options describing how to deal with a type equality
-- in the pure unifier. See 'checkTyEqRhs'
data TyEqFlags a
- = TEF { tef_foralls :: Bool -- Allow foralls
- , tef_lhs :: CanEqLHS -- LHS of the constraint
- , tef_unifying :: AreUnifying -- Always NotUnifying if tef_lhs is TyFamLHS
+ = TEF { tef_task :: TEFTask
+ -- ^ LHS structure, and which checks to perform on the RHS
, tef_fam_app :: TyEqFamApp a
- , tef_occurs :: CheckTyEqProblem } -- Soluble or insoluble occurs check
+ -- ^ How to deal with type family applications
+ }
+
+-- | The structure of the LHS and which checks to perform in 'checkTyEqRhs',
+-- for an equality @lhs ~# rhs at .
+--
+-- See Note [TEFTask].
+data TEFTask
+ -- | LHS is a type family application; we are not unifying.
+ = TEFTyFam
+ { tefTyFam_occursCheck :: CheckTyEqProblem
+ -- ^ The 'CheckTyEqProblem' to report for occurs-check failures
+ -- (soluble or insoluble)
+ , tefTyFam_tyCon :: TyCon
+ , tefTyFam_args :: [Type]
+ }
+ -- | LHS is a 'TyVar'.
+ | TEFTyVar
+ { tefTyVar_occursCheck :: Maybe (Name, CheckTyEqProblem)
+ -- ^ Occurs check: LHS 'TyVar' 'Name',
+ -- and which 'CheckTyEqProblem' to report for occurs-check failures
+ -- (soluble or insoluble)
+ , tefTyVar_levelCheck :: Maybe (TcLevel, LevelCheck)
+ -- ^ Level check: LHS 'TyVar' 'TcLevel',
+ -- and which 'LevelCheck' to perform
+ , tefTyVar_concreteCheck :: Maybe ConcreteTvOrigin
+ -- ^ Concreteness check: LHS 'TyVar' 'ConcreteTvOrigin'
+ -- to use for the check
+ }
+
+{- Note [TEFTask]
+~~~~~~~~~~~~~~~~~
+When we call the pure unifier, e.g. through 'checkTyEqRhs', we can decide what
+kind of checks the unifier performs via the 'TyEqFlags' argument. In particular,
+when the LHS type in a unification is a type variable, we might want to perform
+different checks; this is achieved using the 'TEFTyVar' constructor to 'TEFTask':
+
+ 1. LHS is a skolem tyvar, or an untouchable meta-tyvar.
+ We are not unifying; we only want to perform occurs-checks.
+
+ TEFTyVar
+ { tefTyVar_occursCheck = Just ...
+ , tefTyVar_levelCheck = Nothing
+ , tefTyVar_concreteCheck = Nothing
+ }
+
+ 2. LHS is a touchable meta-tyvar.
+ We are unifying; we want to perform an occurs check, a level check,
+ and a concreteness check (when the meta-tyvar is a ConcreteTv).
+
+ TEFTyVar
+ { tefTyVar_occursCheck = Just ...
+ , tefTyVar_levelCheck = Just ...
+ , tefTyVar_concreteCheck = isConcreteTyVar_maybe lhs_tv
+ }
+
+ 3. LHS is a fresh ConcreteTv meta-tyvar (see call to 'checkTyEqRhs' in
+ 'makeTypeConcrete'). We are unifying; we only want to perform
+ a concreteness check.
+
+ TEFTyVar
+ { tefTyVar_occursCheck = Nothing
+ , tefTyVar_levelCheck = Nothing
+ , tefTyVar_concreteCheck = Just ...
+ }
+-}
+
+-- | Create a "not unifying" 'TEFTask' from a 'CanEqLHS'.
+--
+-- See use-case (1) in Note [TEFTask].
+notUnifying_TEFTask :: CheckTyEqProblem -> CanEqLHS -> TEFTask
+notUnifying_TEFTask occ_prob = \case
+ TyFamLHS tc tys ->
+ TEFTyFam occ_prob tc tys
+ TyVarLHS tv ->
+ TEFTyVar
+ { tefTyVar_occursCheck = Just (tyVarName tv, occ_prob)
+ , tefTyVar_levelCheck = Nothing
+ , tefTyVar_concreteCheck = Nothing
+ }
+ -- We need an occurs-check here, but no level check.
+ -- See Note [Promotion and level-checking] wrinkle (W1)
+
+-- | Create "unifying" 'TEFTask' from a 'TyVarLHS'.
+--
+-- Invariant: the argument 'TyVar' is a 'MetaTv'.
+unifyingLHSMetaTyVar_TEFTask :: TyVar -> LevelCheck -> TEFTask
+unifyingLHSMetaTyVar_TEFTask lhs_tv lc =
+ TEFTyVar
+ { tefTyVar_occursCheck = Just (tyVarName lhs_tv, cteInsolubleOccurs)
+ , tefTyVar_levelCheck = Just (tcTyVarLevel lhs_tv, lc)
+ , tefTyVar_concreteCheck = isConcreteTyVar_maybe lhs_tv
+ }
+
+-- | Do we want to perform a concreteness check in 'checkTyEqRhs'?
+tefTaskConcrete_maybe :: TEFTask -> Maybe ConcreteTvOrigin
+tefTaskConcrete_maybe (TEFTyFam {}) = Nothing
+tefTaskConcrete_maybe (TEFTyVar { tefTyVar_concreteCheck = conc }) = conc
+
+instance Outputable TEFTask where
+ ppr = \case
+ TEFTyFam occ tc tys ->
+ text "TEFTyFam" <+> ppr occ <+> ppr (mkTyConApp tc tys)
+ TEFTyVar mb_occ mb_lc mb_conc ->
+ text "TEFTyVar" <+> hcat (punctuate comma fields)
+ where
+ fields = [ text "OccursCheck:" <+> ppr tv | (tv, _) <- maybeToList mb_occ ]
+ ++
+ [ text "LevelCheck:" <+> ppr lc | lc <- maybeToList mb_lc ]
+ ++
+ [ text "ConcreteCheck" | isJust mb_conc ]
-- | What to do when encountering a type-family application while processing
-- a type equality in the pure unifier.
--
-- See Note [Family applications in canonical constraints]
data TyEqFamApp a
- = TEFA_Fail -- Always fail
- | TEFA_Recurse -- Just recurse
- | TEFA_Break (FamAppBreaker a) -- Recurse, but replace with cycle breaker if fails,
- -- using the FamAppBreaker
-
-data AreUnifying
- = Unifying
- MetaInfo -- MetaInfo of the LHS tyvar (which is a meta-tyvar)
- TcLevel -- Level of the LHS tyvar
- LevelCheck
-
- | NotUnifying -- Not attempting to unify
+ = TEFA_Fail -- ^ Always fail
+ | TEFA_Recurse -- ^ Just recurse
+ | TEFA_Break (FamAppBreaker a) -- ^ Recurse, but replace with cycle breaker if fails,
+ -- using the FamAppBreaker
+-- | What level check to perform, in a call to the pure unifier?
data LevelCheck
- = LC_None -- Level check not needed: we should never encounter
- -- a tyvar at deeper level than the LHS
-
- | LC_Check -- Do a level check between the LHS tyvar and the occurrence tyvar
- -- Fail if the level check fails
-
- | LC_Promote -- Do a level check between the LHS tyvar and the occurrence tyvar
- -- If the level check fails, and the occurrence is a unification
- -- variable, promote it
- Bool -- False <=> don't promote under type families (the common case)
- -- True <=> promote even under type families
- -- see Note [Defaulting equalities] in GHC.Tc.Solver
+ = LC_Check -- ^ Do a level check between the LHS tyvar and the occurrence tyvar.
+ --
+ -- Fail if the level check fails.
+
+ | LC_Promote Bool
+ -- ^ Do a level check between the LHS tyvar and the occurrence tyvar.
+ --
+ -- If the level check fails, and the occurrence is a unification
+ -- variable, promote it.
+ --
+ -- - False <=> don't promote under type families (the common case)
+ -- - True <=> promote even under type families
+ -- (see Note [Defaulting equalities] in GHC.Tc.Solver)
instance Outputable (TyEqFlags a) where
ppr (TEF { .. }) = text "TEF" <> braces (
- vcat [ text "tef_foralls =" <+> ppr tef_foralls
- , text "tef_lhs =" <+> ppr tef_lhs
- , text "tef_unifying =" <+> ppr tef_unifying
- , text "tef_fam_app =" <+> ppr tef_fam_app
- , text "tef_occurs =" <+> ppr tef_occurs ])
+ vcat [ text "tef_task =" <+> ppr tef_task
+ , text "tef_fam_app =" <+> ppr tef_fam_app ])
instance Outputable (TyEqFamApp a) where
ppr TEFA_Fail = text "TEFA_Fail"
ppr TEFA_Recurse = text "TEFA_Recurse"
ppr (TEFA_Break {}) = text "TEFA_Break"
-instance Outputable AreUnifying where
- ppr NotUnifying = text "NotUnifying"
- ppr (Unifying mi lvl lc) = text "Unifying" <+>
- braces (ppr mi <> comma <+> ppr lvl <> comma <+> ppr lc)
-
instance Outputable LevelCheck where
- ppr LC_None = text "LC_None"
ppr LC_Check = text "LC_Check"
ppr (LC_Promote b) = text "LC_Promote" <> ppWhen b (text "(deep)")
+-- | Adjust the 'TyEqFlags' when going undter a type family:
+--
+-- 1. Only the outer family application gets the loop-breaker treatment
+-- 2. Weaken level checks for tyvar promotion. For example, in @[W] alpha[2] ~ Maybe (F beta[3])@,
+-- do not promote @beta[3]@, instead promote @(F beta[3])@.
+-- 3. Occurs checks become potentially soluble (after additional type family
+-- reductions).
famAppArgFlags :: TyEqFlags a -> TyEqFlags a
--- Adjust the flags when going undter a type family
--- Only the outer family application gets the loop-breaker treatment
--- Ditto tyvar promotion. E.g.
--- [W] alpha[2] ~ Maybe (F beta[3])
--- Do not promote beta[3]; instead promote (F beta[3])
-famAppArgFlags flags@(TEF { tef_unifying = unifying })
- = flags { tef_fam_app = TEFA_Recurse
- , tef_unifying = zap_promotion unifying
- , tef_occurs = cteSolubleOccurs }
- -- tef_occurs: under a type family, an occurs check is not definitely-insoluble
+famAppArgFlags flags@(TEF { tef_task = task })
+ = flags { tef_fam_app = TEFA_Recurse -- (1)
+ , tef_task = fam_app_task task
+ }
where
- zap_promotion (Unifying info lvl (LC_Promote deeply))
- | not deeply = Unifying info lvl LC_Check
- zap_promotion unifying = unifying
+ fam_app_task :: TEFTask -> TEFTask
+ fam_app_task task = case task of
+ TEFTyFam {} ->
+ task
+ { tefTyFam_occursCheck = cteSolubleOccurs -- (3)
+ }
+ TEFTyVar { tefTyVar_occursCheck = mb_occ, tefTyVar_levelCheck = mb_lc } ->
+ task
+ { tefTyVar_occursCheck =
+ fmap (\ (tv, _old_occ_prob) -> (tv, cteSolubleOccurs)) mb_occ -- (3)
+ , tefTyVar_levelCheck =
+ fmap (\ (lvl, lc) -> (lvl, zap_lc lc)) mb_lc -- (2)
+ }
+ zap_lc = \case
+ LC_Promote deeply
+ | not deeply
+ -> LC_Check
+ lc -> lc
type FamAppBreaker a = TcType -> TcM (PuResult a Reduction)
-- Given a family-application ty, return a Reduction :: ty ~ cvb
@@ -3196,7 +3314,6 @@ checkTyEqRhs flags ty
FunTy {ft_af = af, ft_mult = w, ft_arg = a, ft_res = r}
| isInvisibleFunArg af -- e.g. Num a => blah
- , not (tef_foralls flags)
-> failCheckWith impredicativeProblem -- Not allowed (TyEq:F)
| otherwise
-> do { w_res <- checkTyEqRhs flags w
@@ -3215,38 +3332,48 @@ checkTyEqRhs flags ty
CoercionTy co -> do { co_res <- checkCo flags co
; return (mkReflCoRedn Nominal <$> co_res) }
- ForAllTy {}
- | tef_foralls flags -> okCheckRefl ty
- | otherwise -> failCheckWith impredicativeProblem -- Not allowed (TyEq:F)
-
+ ForAllTy {} -> failCheckWith impredicativeProblem -- Not allowed (TyEq:F)
-------------------
checkCo :: TyEqFlags a -> Coercion -> TcM (PuResult a Coercion)
-- See Note [checkCo]
-checkCo (TEF { tef_lhs = TyFamLHS {} }) co
- = return (pure co)
-
-checkCo (TEF { tef_lhs = TyVarLHS lhs_tv
- , tef_unifying = unifying
- , tef_occurs = occ_prob }) co
- -- Check for coercion holes, if unifying
- -- See (COERCION-HOLE) in Note [Unification preconditions]
- | hasCoercionHoleCo co
- = failCheckWith (cteProblem cteCoercionHole)
-
- -- Occurs check (can promote)
- | Unifying _ lhs_tv_lvl (LC_Promote {}) <- unifying
- = do { reason <- checkPromoteFreeVars occ_prob lhs_tv lhs_tv_lvl (tyCoVarsOfCo co)
- ; if cterHasNoProblem reason
- then return (pure co)
- else failCheckWith reason }
-
- -- Occurs check (no promotion)
- | lhs_tv `elemVarSet` tyCoVarsOfCo co
- = failCheckWith (cteProblem occ_prob)
+checkCo (TEF { tef_task = task }) co =
+ case task of
+ TEFTyFam {} ->
+ -- NB: 'TEFTyFam' case means we are not unifying.
+ return (pure co)
+ TEFTyVar
+ { tefTyVar_concreteCheck = mb_conc
+ , tefTyVar_levelCheck = mb_lc
+ , tefTyVar_occursCheck = mb_occ
+ }
+ -- Coercions cannot appear in concrete types.
+ --
+ -- See Note [Concrete types] in GHC.Tc.Utils.Concrete.
+ | Just {} <- mb_conc
+ -> failCheckWith (cteProblem cteConcrete)
+
+ -- Check for coercion holes, if unifying.
+ -- See (COERCION-HOLE) in Note [Unification preconditions]
+ | Just {} <- mb_lc -- equivalent to "we are unifying"; see Note [TEFTask]
+ , hasCoercionHoleCo co
+ -> failCheckWith (cteProblem cteCoercionHole)
+
+ -- Occurs check (can promote)
+ | Just (lhs_tv, occ_prob) <- mb_occ
+ , Just (lhs_tv_lvl, LC_Promote {}) <- mb_lc
+ -> do { reason <- checkPromoteFreeVars occ_prob lhs_tv lhs_tv_lvl (tyCoVarsOfCo co)
+ ; if cterHasNoProblem reason
+ then return (pure co)
+ else failCheckWith reason }
+
+ -- Occurs check (no promotion)
+ | Just (lhs_tv, occ_prob) <- mb_occ
+ , nameUnique lhs_tv `elemVarSetByKey` tyCoVarsOfCo co
+ -> failCheckWith (cteProblem occ_prob)
- | otherwise
- = return (pure co)
+ | otherwise
+ -> return (pure co)
{- Note [checkCo]
~~~~~~~~~~~~~~~~~
@@ -3364,7 +3491,7 @@ If we have [W] alpha ~ Maybe (F (G alpha))
checkTyConApp :: TyEqFlags a
-> TcType -> TyCon -> [TcType]
-> TcM (PuResult a Reduction)
-checkTyConApp flags@(TEF { tef_unifying = unifying, tef_foralls = foralls_ok })
+checkTyConApp flags@(TEF { tef_task = task })
tc_app tc tys
| isTypeFamilyTyCon tc
, let arity = tyConArity tc
@@ -3383,11 +3510,10 @@ checkTyConApp flags@(TEF { tef_unifying = unifying, tef_foralls = foralls_ok })
-- See Note [Forgetful synonyms in checkTyConApp]
= checkTyEqRhs flags ty'
- | not (isTauTyCon tc || foralls_ok)
+ | not (isTauTyCon tc)
= failCheckWith impredicativeProblem
- | Unifying info _ _ <- unifying
- , isConcreteInfo info
+ | Just {} <- tefTaskConcrete_maybe task
, not (isConcreteTyCon tc)
= failCheckWith (cteProblem cteConcrete)
@@ -3404,21 +3530,19 @@ checkFamApp :: TyEqFlags a
-> TcType -> TyCon -> [TcType] -- Saturated family application
-> TcM (PuResult a Reduction)
-- See Note [Family applications in canonical constraints]
-checkFamApp flags@(TEF { tef_unifying = unifying, tef_occurs = occ_prob
- , tef_fam_app = fam_app_flag, tef_lhs = lhs })
+checkFamApp flags@(TEF { tef_task = task, tef_fam_app = fam_app_flag })
fam_app tc tys
= case fam_app_flag of
TEFA_Fail -> failCheckWith (cteProblem cteTypeFamily)
-- Occurs check: F ty ~ ...(F ty)...
- _ | TyFamLHS lhs_tc lhs_tys <- lhs
+ _ | TEFTyFam occ_prob lhs_tc lhs_tys <- task
, tcEqTyConApps lhs_tc lhs_tys tc tys
-> case fam_app_flag of
TEFA_Recurse -> failCheckWith (cteProblem occ_prob)
TEFA_Break breaker -> breaker fam_app
- _ | Unifying lhs_info _ _ <- unifying
- , isConcreteInfo lhs_info
+ _ | Just {} <- tefTaskConcrete_maybe task
-> case fam_app_flag of
TEFA_Recurse -> failCheckWith (cteProblem cteConcrete)
TEFA_Break breaker -> breaker fam_app
@@ -3441,22 +3565,55 @@ checkFamApp flags@(TEF { tef_unifying = unifying, tef_occurs = occ_prob
arg_flags = famAppArgFlags flags
-------------------
+
+-- | The result of a single check in 'checkTyVar', such as a concreteness check
+-- or a level check.
+data TyVarCheckResult
+ -- | Check succeded; nothing else to do.
+ = TyVarCheck_Success
+ -- | Check succeeded, but requires an additional promotion.
+ --
+ -- Invariant: at least one of the fields is not 'Nothing'.
+ | TyVarCheck_Promote
+ (Maybe TcLevel)
+ -- ^ @Just lvl@ <=> 'TyVar' needs to be promoted to @lvl@
+ (Maybe ConcreteTvOrigin)
+ -- ^ @Just conc_orig@ <=> 'TyVar' needs to be make concrete
+ -- | Check failed with some 'CheckTyEqProblem's.
+ --
+ -- Invariant: the 'CheckTyEqResult' is not 'cteOK'.
+ | TyVarCheck_Error CheckTyEqResult
+
+instance Semigroup TyVarCheckResult where
+ TyVarCheck_Success <> r = r
+ r <> TyVarCheck_Success = r
+ TyVarCheck_Error e1 <> TyVarCheck_Error e2 =
+ TyVarCheck_Error (e1 S.<> e2)
+ e@(TyVarCheck_Error {}) <> _ = e
+ _ <> e@(TyVarCheck_Error {}) = e
+ TyVarCheck_Promote l1 c1 <> TyVarCheck_Promote l2 c2 =
+ TyVarCheck_Promote
+ (combineMaybe minTcLevel l1 l2)
+ (combineMaybe const c1 c2) -- pick one 'ConcreteTvOrigin' arbitrarily
+
+combineMaybe :: (a -> a -> a) -> Maybe a -> Maybe a -> Maybe a
+combineMaybe _ Nothing r = r
+combineMaybe _ r Nothing = r
+combineMaybe f (Just a) (Just b) = Just (f a b)
+instance Monoid TyVarCheckResult where
+ mempty = TyVarCheck_Success
+
checkTyVar :: forall a. TyEqFlags a -> TcTyVar -> TcM (PuResult a Reduction)
-checkTyVar (TEF { tef_lhs = lhs, tef_unifying = unifying, tef_occurs = occ_prob }) occ_tv
- = case lhs of
- TyFamLHS {} -> success -- Nothing to do if the LHS is a type-family
- TyVarLHS lhs_tv -> check_tv unifying lhs_tv
+checkTyVar flags@(TEF { tef_task = task }) occ_tv
+ = case task of
+ TEFTyFam {} -> success -- Nothing to do if the LHS is a type-family
+ TEFTyVar mb_occ mb_lc mb_conc -> check_tv mb_occ mb_lc mb_conc
where
lvl_occ = tcTyVarLevel occ_tv
success = okCheckRefl (mkTyVarTy occ_tv)
---------------------
- check_tv NotUnifying lhs_tv
- = simple_occurs_check lhs_tv
- -- We need an occurs-check here, but no level check
- -- See Note [Promotion and level-checking] wrinkle (W1)
-
- check_tv (Unifying info lvl prom) lhs_tv
+ check_tv mb_occ mb_lc mb_conc
= do { mb_done <- isFilledMetaTyVar_maybe occ_tv
; case mb_done of
Just {} -> success
@@ -3466,71 +3623,94 @@ checkTyVar (TEF { tef_lhs = lhs, tef_unifying = unifying, tef_occurs = occ_prob
-- a second time; we don't want to re-promote it!
-- Remember, the entire process started with a fully zonked type
- Nothing -> check_unif info lvl prom lhs_tv }
+ Nothing ->
+ do_rhs_checks $
+ -- Occurs check
+ [ simple_occurs_check tv occ_prob | (tv, occ_prob) <- maybeToList mb_occ ]
+ ++
+ -- Level check
+ [ lvl_check lc | lc <- maybeToList mb_lc ]
+ ++
+ -- Concreteness check
+ [ conc_check conc | conc <- maybeToList mb_conc ]
+ }
---------------------
- -- We are in the Unifying branch of AreUnifying; and occ_tv is unfilled
- check_unif :: MetaInfo -> TcLevel -> LevelCheck
- -> TcTyVar -> TcM (PuResult a Reduction)
- check_unif lhs_tv_info lhs_tv_lvl prom lhs_tv
- | isConcreteInfo lhs_tv_info
- , not (isConcreteTyVar occ_tv)
- = if can_make_concrete occ_tv
- then promote lhs_tv lhs_tv_info lhs_tv_lvl
- else failCheckWith (cteProblem cteConcrete)
-
+ simple_occurs_check :: Name -> CheckTyEqProblem -> TyVarCheckResult
+ simple_occurs_check lhs_tv occ_prob
+ | lhs_tv == tyVarName occ_tv || check_kind (tyVarKind occ_tv)
+ = TyVarCheck_Error (cteProblem occ_prob)
+ | otherwise
+ = TyVarCheck_Success
+ where (check_kind, _) = mkOccFolders lhs_tv
+ conc_check :: ConcreteTvOrigin -> TyVarCheckResult
+ conc_check conc_orig
+ | not (isConcreteTyVar occ_tv)
+ = if isMetaTyVar occ_tv
+ then TyVarCheck_Promote Nothing (Just conc_orig)
+ else TyVarCheck_Error (cteProblem cteConcrete)
+ | otherwise
+ = TyVarCheck_Success
+ lvl_check :: (TcLevel, LevelCheck) -> TyVarCheckResult
+ lvl_check (lhs_tv_lvl, lc)
| lvl_occ `strictlyDeeperThan` lhs_tv_lvl
- = case prom of
- LC_None -> pprPanic "check_unif" (ppr lhs_tv $$ ppr occ_tv)
- LC_Check -> failCheckWith (cteProblem cteSkolemEscape)
+ = case lc of
+ LC_Check -> TyVarCheck_Error (cteProblem cteSkolemEscape)
LC_Promote {}
- | isSkolemTyVar occ_tv -> failCheckWith (cteProblem cteSkolemEscape)
- | otherwise -> promote lhs_tv lhs_tv_info lhs_tv_lvl
-
- | otherwise
- = simple_occurs_check lhs_tv
-
- ---------------------
- simple_occurs_check lhs_tv
- | lhs_tv == occ_tv || check_kind (tyVarKind occ_tv)
- = failCheckWith (cteProblem occ_prob)
+ | isSkolemTyVar occ_tv -> TyVarCheck_Error (cteProblem cteSkolemEscape)
+ | otherwise -> TyVarCheck_Promote (Just lhs_tv_lvl) Nothing
| otherwise
- = success
- where
- (check_kind, _) = mkOccFolders lhs_tv
+ = TyVarCheck_Success
- ---------------------
- can_make_concrete occ_tv = case tcTyVarDetails occ_tv of
- MetaTv { mtv_info = info } -> case info of
- ConcreteTv {} -> True
- TauTv {} -> True
- _ -> False
- _ -> False -- Don't attempt to make other type variables concrete
- -- (e.g. SkolemTv, TyVarTv, CycleBreakerTv, RuntimeUnkTv).
+ -- Combine the results of individual checks. See 'TyVarCheckResult'.
+ do_rhs_checks :: [TyVarCheckResult] -> TcM (PuResult a Reduction)
+ do_rhs_checks checks =
+ case mconcat checks of
+ TyVarCheck_Success -> success
+ TyVarCheck_Promote mb_lvl mb_conc -> promote mb_lvl mb_conc
+ TyVarCheck_Error cte_prob -> failCheckWith cte_prob
---------------------
- -- occ_tv is definitely a MetaTyVar
- promote lhs_tv lhs_tv_info lhs_tv_lvl
+ -- occ_tv is definitely a MetaTyVar; we need to promote it/make it concrete
+ promote :: Maybe TcLevel -> Maybe ConcreteTvOrigin -> TcM (PuResult a Reduction)
+ promote mb_lhs_tv_lvl mb_conc
| MetaTv { mtv_info = info_occ, mtv_tclvl = lvl_occ } <- tcTyVarDetails occ_tv
- = do { let new_info | isConcreteInfo lhs_tv_info = lhs_tv_info
- | otherwise = info_occ
- new_lvl = lhs_tv_lvl `minTcLevel` lvl_occ
- -- c[conc,3] ~ p[tau,2]: want to clone p:=p'[conc,2]
- -- c[tau,2] ~ p[tau,3]: want to clone p:=p'[tau,2]
+ = do { let new_info | Just conc <- mb_conc = ConcreteTv conc
+ | otherwise = info_occ
+ new_lvl =
+ case mb_lhs_tv_lvl of
+ Nothing -> lvl_occ
+ Just lhs_tv_lvl -> lhs_tv_lvl `minTcLevel` lvl_occ
+ -- c[conc,3] ~ p[tau,2]: want to clone p:=p'[conc,2]
+ -- c[tau,2] ~ p[tau,3]: want to clone p:=p'[tau,2]
-- Check the kind of occ_tv
- ; reason <- checkPromoteFreeVars occ_prob lhs_tv lhs_tv_lvl (tyCoVarsOfType (tyVarKind occ_tv))
-
- ; if cterHasNoProblem reason -- Successfully promoted
- then do { new_tv_ty <- promote_meta_tyvar new_info new_lvl occ_tv
- ; okCheckRefl new_tv_ty }
- else failCheckWith reason }
+ --
+ -- This is important for several reasons:
+ --
+ -- 1. To ensure there is no occurs check or skolem-escape
+ -- in the kind of occ_tv.
+ -- 2. If the LHS is a concrete type variable and the RHS is an
+ -- unfilled meta-tyvar, we need to ensure that the kind of
+ -- 'occ_tv' is concrete. Test cases: T23051, T23176.
+ ; let occ_kind = tyVarKind occ_tv
+ ; kind_result <- checkTyEqRhs flags occ_kind
+ ; traceTc "checkTyVar: kind check" $
+ vcat [ text "occ_tv:" <+> ppr occ_tv <+> dcolon <+> ppr occ_kind
+ , text "checkTyEqRHS result:" <+> pprPur kind_result
+ ]
+ ; for kind_result $ \ kind_redn ->
+ do { let kind_co = reductionCoercion kind_redn
+ new_kind = reductionReducedType kind_redn
+ ; new_tv_ty <- promote_meta_tyvar new_info new_lvl (setTyVarKind occ_tv new_kind)
+ ; return $ mkGReflLeftRedn Nominal new_tv_ty (mkSymCo kind_co)
+ } }
| otherwise = pprPanic "promote" (ppr occ_tv)
-------------------------
checkPromoteFreeVars :: CheckTyEqProblem -- What occurs check problem to report
- -> TcTyVar -> TcLevel
+ -> Name -> TcLevel
-> TyCoVarSet -> TcM CheckTyEqResult
-- Check this set of TyCoVars for
-- (a) occurs check
@@ -3540,11 +3720,11 @@ checkPromoteFreeVars occ_prob lhs_tv lhs_tv_lvl vs
; return (mconcat oks) }
where
do_one :: TyCoVar -> TcM CheckTyEqResult
- do_one v | isCoVar v = return cteOK
- | lhs_tv == v = return (cteProblem occ_prob)
- | no_promotion = return cteOK
- | not (isMetaTyVar v) = return (cteProblem cteSkolemEscape)
- | otherwise = promote_one v
+ do_one v | isCoVar v = return cteOK
+ | tyVarName v == lhs_tv = return (cteProblem occ_prob)
+ | no_promotion = return cteOK
+ | not (isMetaTyVar v) = return (cteProblem cteSkolemEscape)
+ | otherwise = promote_one v
where
no_promotion = not (tcTyVarLevel v `strictlyDeeperThan` lhs_tv_lvl)
@@ -3606,3 +3786,119 @@ checkTopShape info xi
_ -> False
CycleBreakerTv -> False -- We never unify these
_ -> True
+
+--------------------------------------------------------------------------------
+-- Making a type concrete.
+
+-- | Try to turn the provided type into a concrete type, by ensuring
+-- unfilled metavariables are appropriately marked as concrete.
+--
+-- Returns a coercion whose RHS is a zonked type which is "as concrete as possible",
+-- and a collection of Wanted equality constraints that are necessary to make
+-- the type concrete.
+--
+-- For example, for an input @TYPE a[sk]@ we will return a coercion with RHS
+-- @TYPE gamma[conc]@ together with the Wanted equality constraint @a ~# gamma at .
+--
+-- INVARIANT: the RHS type of the returned coercion is equal to the input type,
+-- up to zonking and the returned Wanted equality constraints.
+--
+-- INVARIANT: if this function returns an empty list of constraints
+-- then the RHS type of the returned coercion is concrete,
+-- in the sense of Note [Concrete types].
+makeTypeConcrete :: FastString -> ConcreteTvOrigin
+ -> TcType -> TcM (TcCoercion, Cts)
+makeTypeConcrete occ_fs conc_orig ty =
+ do { traceTc "makeTypeConcrete {" $
+ vcat [ text "ty:" <+> ppr ty ]
+
+ -- To make a type 'ty' concrete, we query what would happen were we
+ -- to try unifying
+ --
+ -- alpha[conc] ~# ty
+ --
+ -- for a fresh concrete metavariable 'alpha'.
+ --
+ -- We do this by calling 'checkTyEqRhs' with suitable 'TyEqFlags'.
+ -- NB: we don't actually need to create a fresh concrete metavariable
+ -- in order to call 'checkTyEqRhs'.
+ ; let ty_eq_flags =
+ TEF { tef_task =
+ TEFTyVar
+ { tefTyVar_occursCheck = Nothing
+ -- LHS is a fresh meta-tyvar: no occurs check needed
+ , tefTyVar_levelCheck = Nothing
+ , tefTyVar_concreteCheck = Just conc_orig
+ }
+ , tef_fam_app = TEFA_Fail
+ }
+
+ -- NB: 'checkTyEqRhs' expects a fully zonked type as input.
+ ; ty' <- liftZonkM $ zonkTcType ty
+ ; pu_res <- checkTyEqRhs @() ty_eq_flags ty'
+ -- NB: 'checkTyEqRhs' will also check the kind, thus upholding the
+ -- invariant that the kind of a concrete type must also be a concrete type.
+
+ ; (cts, final_co) <-
+ case pu_res of
+ PuOK _ redn ->
+ do { traceTc "makeTypeConcrete: unifier success" $
+ vcat [ text "ty:" <+> ppr ty <+> dcolon <+> ppr (typeKind ty)
+ , text "redn:" <+> ppr redn
+ ]
+ ; return (emptyBag, mkSymCo $ reductionCoercion redn)
+ -- NB: the unifier returns a 'Reduction' with the concrete
+ -- type on the left, but we want a coercion with it on the
+ -- right; so we use 'mkSymCo'.
+ }
+ PuFail _prob ->
+ do { traceTc "makeTypeConcrete: unifier failure" $
+ vcat [ text "ty:" <+> ppr ty <+> dcolon <+> ppr (typeKind ty)
+ , text "problem:" <+> ppr _prob
+ ]
+ -- We failed to make 'ty' concrete. In order to continue
+ -- typechecking, we proceed as follows:
+ --
+ -- - create a new concrete metavariable alpha[conc]
+ -- - emit the equality @ty ~# alpha[conc]@.
+ --
+ -- This equality will eventually get reported as insoluble
+ -- to the user.
+
+ -- The kind of a concrete metavariable must itself be concrete,
+ -- so we need to do a concreteness check on the kind first.
+ ; let ki = typeKind ty
+ ; (kind_co, kind_cts) <-
+ if isConcreteType ki
+ then return (mkNomReflCo ki, emptyBag)
+ else makeTypeConcrete occ_fs conc_orig ki
+
+ -- Now create the new concrete metavariable.
+ ; conc_tv <- newConcreteTyVar conc_orig occ_fs (coercionRKind kind_co)
+ ; let conc_ty = mkTyVarTy conc_tv
+ pty = mkEqPredRole Nominal ty' conc_ty
+ ; hole <- newCoercionHoleO orig pty
+ ; loc <- getCtLocM orig (Just KindLevel)
+ ; let ct = mkNonCanonical
+ $ CtWanted { ctev_pred = pty
+ , ctev_dest = HoleDest hole
+ , ctev_loc = loc
+ , ctev_rewriters = emptyRewriterSet }
+ ; return (kind_cts S.<> unitBag ct, HoleCo hole)
+ }
+
+ ; traceTc "makeTypeConcrete }" $
+ vcat [ text "ty :" <+> _ppr_ty ty
+ , text "ty':" <+> _ppr_ty ty'
+ , text "final_co:" <+> _ppr_co final_co ]
+
+ ; return (final_co, cts)
+ }
+ where
+
+ _ppr_ty ty = ppr ty <+> dcolon <+> ppr (typeKind ty)
+ _ppr_co co = ppr co <+> dcolon <+> parens (_ppr_ty (coercionLKind co)) <+> text "~#" <+> parens (_ppr_ty (coercionRKind co))
+
+ orig :: CtOrigin
+ orig = case conc_orig of
+ ConcreteFRR frr_orig -> FRROrigin frr_orig
=====================================
compiler/GHC/Tc/Utils/Unify.hs-boot
=====================================
@@ -1,11 +1,15 @@
module GHC.Tc.Utils.Unify where
import GHC.Prelude
-import GHC.Core.Type ( Mult )
-import GHC.Tc.Utils.TcType ( TcTauType )
-import GHC.Tc.Types ( TcM )
-import GHC.Tc.Types.Evidence ( TcCoercion )
-import GHC.Tc.Types.Origin ( CtOrigin, TypedThing )
+import GHC.Core.Type ( Mult )
+import GHC.Tc.Utils.TcType ( TcTauType )
+import GHC.Tc.Types ( TcM )
+import GHC.Tc.Types.Constraint ( Cts )
+import GHC.Tc.Types.Evidence ( TcCoercion )
+import GHC.Tc.Types.Origin ( CtOrigin, TypedThing )
+import GHC.Tc.Utils.TcType ( TcType, ConcreteTvOrigin )
+
+import GHC.Data.FastString ( FastString )
-- This boot file exists only to tie the knot between
@@ -15,3 +19,6 @@ unifyType :: Maybe TypedThing -> TcTauType -> TcTauType -> TcM TcCoerci
unifyInvisibleType :: TcTauType -> TcTauType -> TcM TcCoercion
tcSubMult :: CtOrigin -> Mult -> Mult -> TcM ()
+
+makeTypeConcrete :: FastString -> ConcreteTvOrigin
+ -> TcType -> TcM (TcCoercion, Cts)
=====================================
hie.yaml
=====================================
@@ -5,4 +5,4 @@
# cradle: {bios: {program: "./hadrian/hie-bios.bat"}}
#
# The format is documented here - https://github.com/mpickering/hie-bios
-cradle: {bios: {program: "./hadrian/hie-bios"}}
+cradle: {bios: {program: "./hadrian/hie-bios.bat"}}
=====================================
testsuite/tests/rep-poly/RepPolyInferPatBind.stderr
=====================================
@@ -1,4 +1,3 @@
-
RepPolyInferPatBind.hs:21:1: error: [GHC-55287]
The binder ‘x’ does not have a fixed runtime representation.
Its type is:
@@ -8,9 +7,8 @@ RepPolyInferPatBind.hs:21:2: error: [GHC-55287]
• The pattern binding does not have a fixed runtime representation.
Its type is:
T :: TYPE R
- Cannot unify ‘R’ with the type variable ‘c0’
- because the former is not a concrete ‘RuntimeRep’.
• When checking that the pattern signature: T
fits the type of its context: T
In the pattern: x :: T
In a pattern binding: (x :: T) = x
+
=====================================
testsuite/tests/rep-poly/RepPolyInferPatSyn.stderr
=====================================
@@ -1,12 +1,10 @@
-
RepPolyInferPatSyn.hs:22:16: error: [GHC-55287]
• The pattern synonym argument pattern
does not have a fixed runtime representation.
Its type is:
T :: TYPE R
- Cannot unify ‘R’ with the type variable ‘c0’
- because the former is not a concrete ‘RuntimeRep’.
• When checking that the pattern signature: T
fits the type of its context: T
In the pattern: a :: T
In the declaration for pattern synonym ‘P’
+
=====================================
testsuite/tests/rep-poly/RepPolyTuple3.stderr
=====================================
@@ -1,6 +1,6 @@
-
RepPolyTuple3.hs:21:9: error: [GHC-18872]
• Couldn't match kind ‘FloatRep’ with ‘IntRep’
arising from a representation-polymorphism check
• In the expression: (#,#) @RR @RR x
In an equation for ‘bar’: bar x = (#,#) @RR @RR x
+
=====================================
testsuite/tests/rep-poly/T23153.stderr
=====================================
@@ -1,4 +1,3 @@
-
T23153.hs:8:1: error: [GHC-52083]
The argument ‘(h ())’ of ‘f’
cannot be assigned a fixed runtime representation, not even by defaulting.
@@ -13,3 +12,4 @@ T23153.hs:8:1: error: [GHC-52083]
The argument ‘(h ())’ of ‘f’
cannot be assigned a fixed runtime representation, not even by defaulting.
Suggested fix: Add a type signature.
+
=====================================
testsuite/tests/rep-poly/T23154.stderr
=====================================
@@ -1,3 +1,7 @@
+T23154.hs:7:1: error: [GHC-52083]
+ The first pattern in the equation for ‘f’
+ cannot be assigned a fixed runtime representation, not even by defaulting.
+ Suggested fix: Add a type signature.
T23154.hs:7:1: error: [GHC-52083]
The first pattern in the equation for ‘f’
@@ -8,3 +12,4 @@ T23154.hs:7:1: error: [GHC-52083]
The first pattern in the equation for ‘f’
cannot be assigned a fixed runtime representation, not even by defaulting.
Suggested fix: Add a type signature.
+
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/87e82e2efd72fffefbc9537b5ab86611279e009a
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/87e82e2efd72fffefbc9537b5ab86611279e009a
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/20250117/3892b351/attachment-0001.html>
More information about the ghc-commits
mailing list