From 268efcc9a45da36458442d9203c66a415b48f2b3 Mon Sep 17 00:00:00 2001 From: Matthew Pickering Date: Tue, 30 Nov 2021 17:05:11 +0000 Subject: Rework the handling of SkolemInfo The main purpose of this patch is to attach a SkolemInfo directly to each SkolemTv. This fixes the large number of bugs which have accumulated over the years where we failed to report errors due to having "no skolem info" for particular type variables. Now the origin of each type varible is stored on the type variable we can always report accurately where it cames from. Fixes #20969 #20732 #20680 #19482 #20232 #19752 #10946 #19760 #20063 #13499 #14040 The main changes of this patch are: * SkolemTv now contains a SkolemInfo field which tells us how the SkolemTv was created. Used when reporting errors. * Enforce invariants relating the SkolemInfoAnon and level of an implication (ic_info, ic_tclvl) to the SkolemInfo and level of the type variables in ic_skols. * All ic_skols are TcTyVars -- Check is currently disabled * All ic_skols are SkolemTv * The tv_lvl of the ic_skols agrees with the ic_tclvl * The ic_info agrees with the SkolInfo of the implication. These invariants are checked by a debug compiler by checkImplicationInvariants. * Completely refactor kcCheckDeclHeader_sig which kept doing my head in. Plus, it wasn't right because it wasn't skolemising the binders as it decomposed the kind signature. The new story is described in Note [kcCheckDeclHeader_sig]. The code is considerably shorter than before (roughly 240 lines turns into 150 lines). It still has the same awkward complexity around computing arity as before, but that is a language design issue. See Note [Arity inference in kcCheckDeclHeader_sig] * I added new type synonyms MonoTcTyCon and PolyTcTyCon, and used them to be clear which TcTyCons have "finished" kinds etc, and which are monomorphic. See Note [TcTyCon, MonoTcTyCon, and PolyTcTyCon] * I renamed etaExpandAlgTyCon to splitTyConKind, becuase that's a better name, and it is very useful in kcCheckDeclHeader_sig, where eta-expansion isn't an issue. * Kill off the nasty `ClassScopedTvEnv` entirely. Co-authored-by: Simon Peyton Jones --- testsuite/tests/typecheck/should_fail/T15629.stderr | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) (limited to 'testsuite/tests/typecheck/should_fail/T15629.stderr') diff --git a/testsuite/tests/typecheck/should_fail/T15629.stderr b/testsuite/tests/typecheck/should_fail/T15629.stderr index c1d751bee2..aabc868844 100644 --- a/testsuite/tests/typecheck/should_fail/T15629.stderr +++ b/testsuite/tests/typecheck/should_fail/T15629.stderr @@ -6,21 +6,21 @@ T15629.hs:26:31: error: (F x ab) (F x z) -> *’ ‘z’ is a rigid type variable bound by - an explicit forall z ab + the type signature for ‘g’ at T15629.hs:26:17 ‘ab’ is a rigid type variable bound by - an explicit forall z ab + the type signature for ‘g’ at T15629.hs:26:19-20 • In the first argument of ‘Proxy’, namely ‘((Comp (F1Sym :: x ~> F x z) F2Sym) :: F x ab ~> F x ab)’ In the type signature: - g :: forall z ab. - Proxy ((Comp (F1Sym :: x ~> F x z) F2Sym) :: F x ab ~> F x ab) + g :: forall z ab. Proxy ((Comp (F1Sym :: x + ~> F x z) F2Sym) :: F x ab ~> F x ab) In an equation for ‘f’: f _ = () where g :: - forall z ab. - Proxy ((Comp (F1Sym :: x ~> F x z) F2Sym) :: F x ab ~> F x ab) + forall z ab. Proxy ((Comp (F1Sym :: x ~> F x z) F2Sym) :: F x ab + ~> F x ab) g = sg Proxy Proxy -- cgit v1.2.1