[Git][ghc/ghc][wip/repr-invariant] Alternative fix for 23883
Krzysztof Gogolewski (@monoidal)
gitlab at gitlab.haskell.org
Thu Sep 21 22:04:39 UTC 2023
Krzysztof Gogolewski pushed to branch wip/repr-invariant at Glasgow Haskell Compiler / GHC
Commits:
c73e8e45 by Krzysztof Gogolewski at 2023-09-22T00:04:30+02:00
Alternative fix for 23883
- - - - -
11 changed files:
- compiler/GHC/Tc/Gen/App.hs
- compiler/GHC/Tc/Utils/Concrete.hs
- testsuite/tests/rep-poly/RepPolyInferPatBind.stderr
- testsuite/tests/rep-poly/RepPolyInferPatSyn.stderr
- + testsuite/tests/rep-poly/T23883a.hs
- + testsuite/tests/rep-poly/T23883a.stderr
- + testsuite/tests/rep-poly/T23883b.hs
- + testsuite/tests/rep-poly/T23883b.stderr
- + testsuite/tests/rep-poly/T23883c.hs
- + testsuite/tests/rep-poly/T23883c.stderr
- testsuite/tests/rep-poly/all.T
Changes:
=====================================
compiler/GHC/Tc/Gen/App.hs
=====================================
@@ -30,7 +30,7 @@ import GHC.Tc.Utils.Unify
import GHC.Tc.Utils.Instantiate
import GHC.Tc.Instance.Family ( tcGetFamInstEnvs, tcLookupDataFamInst_maybe )
import GHC.Tc.Gen.HsType
-import GHC.Tc.Utils.Concrete ( unifyConcrete, idConcreteTvs )
+import GHC.Tc.Utils.Concrete ( unifyConcrete_rep, idConcreteTvs )
import GHC.Tc.Utils.TcMType
import GHC.Tc.Types.Evidence
import GHC.Tc.Types.Origin
@@ -839,7 +839,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
+ do { mco <- unifyConcrete_rep (occNameFS $ getOccName $ tv_nm) conc ty_arg0
; return $ case mco of { MRefl -> ty_arg0; MCo co -> coercionRKind co } }
; let fun_ty = mkForAllTy tvb inner_ty
=====================================
compiler/GHC/Tc/Utils/Concrete.hs
=====================================
@@ -10,7 +10,8 @@ module GHC.Tc.Utils.Concrete
hasFixedRuntimeRep
, hasFixedRuntimeRep_syntactic
- , unifyConcrete
+ , unifyConcrete_kind
+ , unifyConcrete_rep
, idConcreteTvs
)
@@ -19,13 +20,15 @@ module GHC.Tc.Utils.Concrete
import GHC.Prelude
import GHC.Builtin.Names ( unsafeCoercePrimName )
-import GHC.Builtin.Types ( liftedTypeKindTyCon, unliftedTypeKindTyCon )
+import GHC.Builtin.Types ( liftedTypeKindTyCon, unliftedTypeKindTyCon, runtimeRepTy )
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.Type ( isConcreteType, typeKind, mkFunTy,
+ typeOrConstraintKind, typeTypeOrConstraint,
+ sORTKind_maybe )
import GHC.Tc.Types.Constraint ( NotConcreteError(..), NotConcreteReason(..) )
import GHC.Tc.Types.Evidence ( Role(..), TcCoercionN, TcMCoercionN )
@@ -43,10 +46,12 @@ import GHC.Types.Var ( tyVarKind, tyVarName )
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.Maybe ( isJust )
import Data.Functor ( ($>) )
import Data.List.NonEmpty ( NonEmpty((:|)) )
@@ -405,7 +410,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 (unifyConcrete_kind (fsLit "cx") . ConcreteFRR) frr_ctxt ty
-- | Like 'hasFixedRuntimeRep', but we perform an eager syntactic check.
--
@@ -489,9 +494,30 @@ checkFRR_with check_kind frr_ctxt ty
--
-- We assume the provided type is already at the kind-level
-- (this only matters for error messages).
-unifyConcrete :: HasDebugCallStack
+unifyConcrete_kind :: HasDebugCallStack
=> FastString -> ConcreteTvOrigin -> TcType -> TcM TcMCoercionN
-unifyConcrete occ_fs conc_orig ty
+unifyConcrete_kind occ_fs conc_orig ty
+ = do { massertPpr (isJust $ sORTKind_maybe ty) (ppr ty)
+ ; (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 runtimeRepTy
+ ; coToMCo <$> emitWantedEq orig KindLevel Nominal ty (typeOrConstraintKind (typeTypeOrConstraint ty) (mkTyVarTy conc_tv)) } } }
+ where
+ orig :: CtOrigin
+ orig = case conc_orig of
+ ConcreteFRR frr_orig -> FRROrigin frr_orig
+
+unifyConcrete_rep :: HasDebugCallStack
+ => FastString -> ConcreteTvOrigin -> TcType -> TcM TcMCoercionN
+unifyConcrete_rep occ_fs conc_orig ty
= do { (ty, errs) <- makeTypeConcrete conc_orig ty
; case errs of
-- We were able to make the type fully concrete.
=====================================
testsuite/tests/rep-poly/RepPolyInferPatBind.stderr
=====================================
@@ -8,8 +8,6 @@ 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
=====================================
testsuite/tests/rep-poly/RepPolyInferPatSyn.stderr
=====================================
@@ -4,8 +4,6 @@ RepPolyInferPatSyn.hs:22:16: error: [GHC-55287]
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
=====================================
testsuite/tests/rep-poly/T23883a.hs
=====================================
@@ -0,0 +1,6 @@
+module T23883a where
+
+import GHC.Exts
+
+setField :: forall a_rep (a :: TYPE a_rep). a -> Int
+setField x = undefined (\ _ -> x)
=====================================
testsuite/tests/rep-poly/T23883a.stderr
=====================================
@@ -0,0 +1,6 @@
+
+T23883a.hs:6:1: error: [GHC-55287]
+ The first pattern in the equation for ‘setField’
+ does not have a fixed runtime representation.
+ Its type is:
+ a :: TYPE a_rep
=====================================
testsuite/tests/rep-poly/T23883b.hs
=====================================
@@ -0,0 +1,6 @@
+module T23883b where
+
+import GHC.Exts
+
+setField :: forall a_rep (a :: TYPE a_rep). a -> ()
+setField x _ = ()
=====================================
testsuite/tests/rep-poly/T23883b.stderr
=====================================
@@ -0,0 +1,5 @@
+
+T23883b.hs:6:1: error: [GHC-83865]
+ • Couldn't match expected type ‘()’ with actual type ‘p0 -> ()’
+ • The equation for ‘setField’ has two value arguments,
+ but its type ‘a -> ()’ has only one
=====================================
testsuite/tests/rep-poly/T23883c.hs
=====================================
@@ -0,0 +1,6 @@
+module T23883c where
+
+import GHC.Exts
+
+setField :: forall r s (a :: TYPE (r s)). a -> ()
+setField x _ = ()
=====================================
testsuite/tests/rep-poly/T23883c.stderr
=====================================
@@ -0,0 +1,5 @@
+
+T23883c.hs:6:1: error: [GHC-83865]
+ • Couldn't match expected type ‘()’ with actual type ‘p0 -> ()’
+ • The equation for ‘setField’ has two value arguments,
+ but its type ‘a -> ()’ has only one
=====================================
testsuite/tests/rep-poly/all.T
=====================================
@@ -106,6 +106,10 @@ test('RepPolyWrappedVar2', [js_skip], compile, [''])
test('UnliftedNewtypesCoerceFail', normal, compile_fail, [''])
test('UnliftedNewtypesLevityBinder', normal, compile_fail, [''])
+test('T23883a', normal, compile_fail, [''])
+test('T23883b', normal, compile_fail, [''])
+test('T23883c', normal, compile_fail, [''])
+
###############################################################################
## The following tests require rewriting in RuntimeReps, ##
## i.e. PHASE 2 of the FixedRuntimeRep plan. ##
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/c73e8e45f9395c21df40df6bc2eac4eab78487e4
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/c73e8e45f9395c21df40df6bc2eac4eab78487e4
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/20230921/0a6a6171/attachment-0001.html>
More information about the ghc-commits
mailing list