[commit: ghc] master: Improve rejigConRes (again) (a870738)
git at git.haskell.org
git at git.haskell.org
Fri Sep 11 16:17:19 UTC 2015
Repository : ssh://git@git.haskell.org/ghc
On branch : master
Link : http://ghc.haskell.org/trac/ghc/changeset/a870738a3b34d264c63656783e84168a230d7da4/ghc
>---------------------------------------------------------------
commit a870738a3b34d264c63656783e84168a230d7da4
Author: Simon Peyton Jones <simonpj at microsoft.com>
Date: Fri Sep 11 15:54:39 2015 +0100
Improve rejigConRes (again)
I think this patch finally works around the delicacy in the strictness
of TcTyClsDecls.rejigConRes. See the notes with that function and
Note [Checking GADT return types].
As a result, we fix Trac #10836, and improve Trac #7175
>---------------------------------------------------------------
a870738a3b34d264c63656783e84168a230d7da4
compiler/typecheck/TcTyClsDecls.hs | 67 +++++++++++++---------
testsuite/tests/typecheck/should_fail/T7175.stderr | 6 ++
testsuite/tests/typecheck/should_fail/all.T | 2 +-
3 files changed, 46 insertions(+), 29 deletions(-)
diff --git a/compiler/typecheck/TcTyClsDecls.hs b/compiler/typecheck/TcTyClsDecls.hs
index 19af9f0..11dc141 100644
--- a/compiler/typecheck/TcTyClsDecls.hs
+++ b/compiler/typecheck/TcTyClsDecls.hs
@@ -162,10 +162,8 @@ tcTyClGroup tyclds
-- expects well-formed TyCons
; tcExtendGlobalEnv tyclss $ do
{ traceTc "Starting validity check" (ppr tyclss)
- ; checkNoErrs $
- mapM_ (recoverM (return ()) . checkValidTyCl) tyclss
+ ; mapM_ (recoverM (return ()) . checkValidTyCl) tyclss
-- We recover, which allows us to report multiple validity errors
- -- the checkNoErrs is necessary to fix #7175.
; mapM_ (recoverM (return ()) . checkValidRoleAnnots role_annots) tyclss
-- See Note [Check role annotations in a second pass]
@@ -1285,6 +1283,9 @@ tcConDecl new_or_data rep_tycon tmpl_tvs res_tmpl -- Data types
ResTyGADT ls ty -> ResTyGADT ls <$> zonkTcTypeToType ze ty
; let (univ_tvs, ex_tvs, eq_preds, res_ty') = rejigConRes tmpl_tvs res_tmpl qtkvs res_ty
+ -- NB: this is a /lazy/ binding, so we pass four thunks to buildDataCon
+ -- without yet forcing the guards in rejigConRes
+ -- See Note [Checking GADT return types]
; fam_envs <- tcGetFamInstEnvs
; let
@@ -1375,7 +1376,7 @@ There is a delicacy around checking the return types of a datacon. The
central problem is dealing with a declaration like
data T a where
- MkT :: a -> Q a
+ MkT :: T a -> Q a
Note that the return type of MkT is totally bogus. When creating the T
tycon, we also need to create the MkT datacon, which must have a "rejigged"
@@ -1383,14 +1384,17 @@ return type. That is, the MkT datacon's type must be transformed to have
a uniform return type with explicit coercions for GADT-like type parameters.
This rejigging is what rejigConRes does. The problem is, though, that checking
that the return type is appropriate is much easier when done over *Type*,
-not *HsType*.
-
-So, we want to make rejigConRes lazy and then check the validity of the return
-type in checkValidDataCon. But, if the return type is bogus, rejigConRes can't
-work -- it will have a failed pattern match. Luckily, if we run
-checkValidDataCon before ever looking at the rejigged return type
-(checkValidDataCon checks the dataConUserType, which is not rejigged!), we
-catch the error before forcing the rejigged type and panicking.
+not *HsType*, and doing a call to tcMatchTy will loop because T isn't fully
+defined yet.
+
+So, we want to make rejigConRes lazy and then check the validity of
+the return type in checkValidDataCon. To do this we /always/ return a
+4-tuple from rejigConRes (so that we can extract ret_ty from it, which
+checkValidDataCon needs), but the first three fields may be bogus if
+the return type isn't valid (the last equation for rejigConRes).
+
+This is better than an earlier solution which reduced the number of
+errors reported in one pass. See Trac #7175, and #10836.
-}
-- Example
@@ -1432,20 +1436,27 @@ rejigConRes tmpl_tvs res_tmpl dc_tvs (ResTyGADT _ res_ty)
-- z
-- Existentials are the leftover type vars: [x,y]
-- So we return ([a,b,z], [x,y], [a~(x,y),b~z], T [(x,y)] z z)
+ | Just subst <- tcMatchTy (mkVarSet tmpl_tvs) res_tmpl res_ty
+ , (univ_tvs, eq_spec) <- foldr (choose subst) ([], []) tmpl_tvs
+ , let ex_tvs = dc_tvs `minusList` univ_tvs
= (univ_tvs, ex_tvs, eq_spec, res_ty)
+
+ | otherwise
+ -- If the return type of the data constructor doesn't match the parent
+ -- type constructor, or the arity is wrong, the tcMatchTy will fail
+ -- e.g data T a b where
+ -- T1 :: Maybe a -- Wrong tycon
+ -- T2 :: T [a] -- Wrong arity
+ -- We are detect that later, in checkValidDataCon, but meanwhile
+ -- we must do *something*, not just crash. So we do something simple
+ -- albeit bogus, relying on checkValidDataCon to check the
+ -- bad-result-type error before seeing that the other fields look odd
+ -- See Note [Checking GADT return types]
+ = (tmpl_tvs, dc_tvs `minusList` tmpl_tvs, [], res_ty)
where
- Just subst = tcMatchTy (mkVarSet tmpl_tvs) res_tmpl res_ty
- -- This 'Just' pattern is sure to match, because if not
- -- checkValidDataCon will complain first.
- -- But care: this only works if the result of rejigConRes
- -- is not demanded until checkValidDataCon has
- -- first succeeded
- -- See Note [Checking GADT return types]
-
- -- /Lazily/ figure out the univ_tvs etc
- -- Each univ_tv is either a dc_tv or a tmpl_tv
- (univ_tvs, eq_spec) = foldr choose ([], []) tmpl_tvs
- choose tmpl (univs, eqs)
+ -- Figure out the univ_tvs etc
+ -- Each univ_tv is either a dc_tv or a tmpl_tv
+ choose subst tmpl (univs, eqs)
| Just ty <- lookupTyVar subst tmpl
= case tcGetTyVar_maybe ty of
Just tv | not (tv `elem` univs)
@@ -1454,7 +1465,6 @@ rejigConRes tmpl_tvs res_tmpl dc_tvs (ResTyGADT _ res_ty)
where -- see Note [Substitution in template variables kinds]
new_tmpl = updateTyVarKind (substTy subst) tmpl
| otherwise = pprPanic "tcResultType" (ppr res_ty)
- ex_tvs = dc_tvs `minusList` univ_tvs
{-
Note [Substitution in template variables kinds]
@@ -1633,9 +1643,10 @@ checkValidDataCon dflags existential_ok tc con
do { -- Check that the return type of the data constructor
-- matches the type constructor; eg reject this:
-- data T a where { MkT :: Bogus a }
- -- c.f. Note [Check role annotations in a second pass]
- -- and Note [Checking GADT return types]
- let tc_tvs = tyConTyVars tc
+ -- It's important to do this first:
+ -- see Note [Checking GADT return types]
+ -- and c.f. Note [Check role annotations in a second pass]
+ let tc_tvs = tyConTyVars tc
res_ty_tmpl = mkFamilyTyConApp tc (mkTyVarTys tc_tvs)
orig_res_ty = dataConOrigResTy con
; traceTc "checkValidDataCon" (vcat
diff --git a/testsuite/tests/typecheck/should_fail/T7175.stderr b/testsuite/tests/typecheck/should_fail/T7175.stderr
index 25e9365..57d798f 100644
--- a/testsuite/tests/typecheck/should_fail/T7175.stderr
+++ b/testsuite/tests/typecheck/should_fail/T7175.stderr
@@ -4,3 +4,9 @@ T7175.hs:8:4: error:
instead of an instance of its parent type ‘G1 a’
In the definition of data constructor ‘G1C’
In the data type declaration for ‘G1’
+
+T7175.hs:11:4: error:
+ Data constructor ‘G2C’ returns type ‘F Int’
+ instead of an instance of its parent type ‘G2 a’
+ In the definition of data constructor ‘G2C’
+ In the data type declaration for ‘G2’
diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T
index 66b8a86..31646d6 100644
--- a/testsuite/tests/typecheck/should_fail/all.T
+++ b/testsuite/tests/typecheck/should_fail/all.T
@@ -395,4 +395,4 @@ test('ExpandSynsFail2', normal, compile_fail, ['-fprint-expanded-synonyms'])
test('ExpandSynsFail3', normal, compile_fail, ['-fprint-expanded-synonyms'])
test('ExpandSynsFail4', normal, compile_fail, ['-fprint-expanded-synonyms'])
test('T10698', expect_broken(10698), compile_fail, [''])
-test('T10836', expect_broken(10836), compile_fail, [''])
+test('T10836', normal, compile_fail, [''])
More information about the ghc-commits
mailing list