[Git][ghc/ghc][wip/T23070-unify] 2 commits: Wibble error messages
Simon Peyton Jones (@simonpj)
gitlab at gitlab.haskell.org
Wed Apr 12 08:37:31 UTC 2023
Simon Peyton Jones pushed to branch wip/T23070-unify at Glasgow Haskell Compiler / GHC
Commits:
e98151ce by Simon Peyton Jones at 2023-04-12T09:37:50+01:00
Wibble error messages
- - - - -
8e27d540 by Simon Peyton Jones at 2023-04-12T09:38:13+01:00
Experimental change: coercion holes
Experiment with making a constraint non-canonical if it has
a coercion hole on the RHS.
Simplifies T22707 a lot!
- - - - -
11 changed files:
- compiler/GHC/Tc/Solver/InertSet.hs
- compiler/GHC/Tc/Solver/Interact.hs
- compiler/GHC/Tc/Solver/Monad.hs
- compiler/GHC/Tc/Types/Origin.hs
- compiler/GHC/Tc/Utils/Concrete.hs
- compiler/GHC/Tc/Utils/Unify.hs
- testsuite/tests/polykinds/T9017.stderr
- testsuite/tests/typecheck/should_fail/T21530a.stderr
- testsuite/tests/typecheck/should_fail/T3950.stderr
- testsuite/tests/typecheck/should_fail/T7368.stderr
- testsuite/tests/typecheck/should_fail/T7368a.stderr
Changes:
=====================================
compiler/GHC/Tc/Solver/InertSet.hs
=====================================
@@ -8,7 +8,8 @@ module GHC.Tc.Solver.InertSet (
-- * The work list
WorkList(..), isEmptyWorkList, emptyWorkList,
extendWorkListNonEq, extendWorkListCt,
- extendWorkListCts, extendWorkListEq, extendWorkListEqs,
+ extendWorkListCts, extendWorkListCtList,
+ extendWorkListEq, extendWorkListEqs,
appendWorkList, extendWorkListImplic,
workListSize,
selectWorkItem,
@@ -192,7 +193,7 @@ extendWorkListImplic :: Implication -> WorkList -> WorkList
extendWorkListImplic implic wl = wl { wl_implics = implic `consBag` wl_implics wl }
extendWorkListCt :: Ct -> WorkList -> WorkList
--- Agnostic
+-- Agnostic about what kind of constraint
extendWorkListCt ct wl
= case classifyPredType (ctPred ct) of
EqPred {}
@@ -204,8 +205,10 @@ extendWorkListCt ct wl
_ -> extendWorkListNonEq ct wl
-extendWorkListCts :: [Ct] -> WorkList -> WorkList
--- Agnostic
+extendWorkListCtList :: [Ct] -> WorkList -> WorkList
+extendWorkListCtList cts wl = foldr extendWorkListCt wl cts
+
+extendWorkListCts :: Cts -> WorkList -> WorkList
extendWorkListCts cts wl = foldr extendWorkListCt wl cts
isEmptyWorkList :: WorkList -> Bool
@@ -1331,11 +1334,11 @@ kickOutRewritableLHS new_fr new_lhs
-- constraints, which perhaps may have become soluble after new_lhs
-- is substituted; ditto the dictionaries, which may include (a~b)
-- or (a~~b) constraints.
- kicked_out = foldr extendWorkListCt
- (emptyWorkList { wl_eqs = map CEqCan tv_eqs_out ++
- map CEqCan feqs_out })
+ kicked_out = extendWorkListCts
((dicts_out `andCts` irs_out)
`extendCtsList` insts_out)
+ (emptyWorkList { wl_eqs = map CEqCan tv_eqs_out ++
+ map CEqCan feqs_out })
(tv_eqs_out, tv_eqs_in) = partitionInertEqs kick_out_eq tv_eqs
(feqs_out, feqs_in) = partitionFunEqs kick_out_eq funeqmap
=====================================
compiler/GHC/Tc/Solver/Interact.hs
=====================================
@@ -153,7 +153,7 @@ solveSimples :: Cts -> TcS ()
solveSimples cts
= {-# SCC "solveSimples" #-}
- do { updWorkListTcS (\wl -> foldr extendWorkListCt wl cts)
+ do { updWorkListTcS (extendWorkListCts cts)
; solve_loop }
where
solve_loop
=====================================
compiler/GHC/Tc/Solver/Monad.hs
=====================================
@@ -168,6 +168,7 @@ import GHC.Types.Name.Reader
import GHC.Types.Var
import GHC.Types.Var.Set
import GHC.Types.Unique.Supply
+import GHC.Types.Unique.Set( elementOfUniqSet )
import GHC.Unit.Module ( HasModule, getModule, extractModule )
import qualified GHC.Rename.Env as TcM
@@ -422,10 +423,10 @@ kickOutAfterFillingCoercionHole :: CoercionHole -> TcS ()
kickOutAfterFillingCoercionHole hole
= do { ics <- getInertCans
; let (kicked_out, ics') = kick_out ics
- n_kicked = workListSize kicked_out
+ n_kicked = lengthBag kicked_out
; unless (n_kicked == 0) $
- do { updWorkListTcS (appendWorkList kicked_out)
+ do { updWorkListTcS (extendWorkListCts kicked_out)
; csTraceTcS $
hang (text "Kick out, hole =" <+> ppr hole)
2 (vcat [ text "n-kicked =" <+> int n_kicked
@@ -434,19 +435,39 @@ kickOutAfterFillingCoercionHole hole
; setInertCans ics' }
where
+ kick_out :: InertCans -> (Cts, InertCans)
+ kick_out ics@(IC { inert_irreds = irreds })
+ = (irreds_to_kick, ics { inert_irreds = irreds_to_keep })
+ where
+ (irreds_to_kick, irreds_to_keep) = partitionBag kick_ct irreds
+
+ kick_ct :: Ct -> Bool
+ -- True: kick out; False: keep.
+ kick_ct ct
+ | CIrredCan { cc_ev = ev, cc_reason = reason } <- ct
+ , CtWanted { ctev_rewriters = RewriterSet rewriters } <- ev
+ , NonCanonicalReason ctyeq <- reason
+ , ctyeq `cterHasProblem` cteCoercionHole
+ , hole `elementOfUniqSet` rewriters
+ = True
+ | otherwise
+ = False
+
+{-
kick_out :: InertCans -> (WorkList, InertCans)
kick_out ics@(IC { inert_eqs = eqs, inert_funeqs = funeqs })
= (kicked_out, ics { inert_eqs = eqs_to_keep, inert_funeqs = funeqs_to_keep })
where
(eqs_to_kick, eqs_to_keep) = partitionInertEqs kick_ct eqs
(funeqs_to_kick, funeqs_to_keep) = partitionFunEqs kick_ct funeqs
- kicked_out = extendWorkListCts (map CEqCan (eqs_to_kick ++ funeqs_to_kick)) emptyWorkList
+ kicked_out = extendWorkListCtList (map CEqCan (eqs_to_kick ++ funeqs_to_kick)) emptyWorkList
kick_ct :: EqCt -> Bool
-- True: kick out; False: keep.
kick_ct (EqCt { eq_rhs = rhs, eq_ev = ctev })
= isWanted ctev && -- optimisation: givens don't have coercion holes anyway
rhs `hasThisCoercionHoleTy` hole
+-}
--------------
addInertSafehask :: InertCans -> Ct -> InertCans
@@ -1259,7 +1280,7 @@ emitWork :: [Ct] -> TcS ()
emitWork [] = return () -- avoid printing, among other work
emitWork cts
= do { traceTcS "Emitting fresh work" (vcat (map ppr cts))
- ; updWorkListTcS (extendWorkListCts cts) }
+ ; updWorkListTcS (extendWorkListCtList cts) }
emitImplication :: Implication -> TcS ()
emitImplication implic
=====================================
compiler/GHC/Tc/Types/Origin.hs
=====================================
@@ -1000,6 +1000,11 @@ data FixedRuntimeRepOrigin
-- ^ What context requires a fixed runtime representation?
}
+instance Outputable FixedRuntimeRepOrigin where
+ ppr (FixedRuntimeRepOrigin { frr_type = ty, frr_context = cxt })
+ = text "FrOrigin" <> braces (vcat [ text "frr_type:" <+> ppr ty
+ , text "frr_context:" <+> ppr cxt ])
+
-- | The context in which a representation-polymorphism check was performed.
--
-- Does not include the type on which the check was performed; see
=====================================
compiler/GHC/Tc/Utils/Concrete.hs
=====================================
@@ -524,7 +524,8 @@ ensureConcrete :: HasDebugCallStack
-> TcType
-> TcM TcType
ensureConcrete frr_orig ty
- = do { (ty', errs) <- makeTypeConcrete conc_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" $
=====================================
compiler/GHC/Tc/Utils/Unify.hs
=====================================
@@ -2931,8 +2931,8 @@ checkCo (TEF { tef_lhs = TyVarLHS lhs_tv
, tef_occurs = occ_prob }) co
-- Check for coercion holes, if unifying
-- See (COERCION-HOLE) in Note [Unification preconditions]
- | Unifying {} <- unifying
- , hasCoercionHoleCo co
+ | -- Unifying {} <- unifying
+ hasCoercionHoleCo co
= failCheckWith (cteProblem cteCoercionHole)
-- Occurs check (can promote)
=====================================
testsuite/tests/polykinds/T9017.stderr
=====================================
@@ -1,12 +1,12 @@
T9017.hs:8:7: error: [GHC-25897]
- • Couldn't match kind ‘k2’ with ‘*’
+ • Couldn't match kind ‘k1’ with ‘*’
When matching types
a0 :: * -> * -> *
a :: k1 -> k2 -> *
Expected: a b (m b)
Actual: a0 b0 (m0 b0)
- ‘k2’ is a rigid type variable bound by
+ ‘k1’ is a rigid type variable bound by
the type signature for:
foo :: forall {k1} {k2} (a :: k1 -> k2 -> *) (b :: k1)
(m :: k1 -> k2).
=====================================
testsuite/tests/typecheck/should_fail/T21530a.stderr
=====================================
@@ -1,6 +1,6 @@
T21530a.hs:14:7: error: [GHC-18872]
- • Couldn't match kind ‘*’ with ‘Constraint’
+ • Couldn't match kind ‘Constraint’ with ‘*’
When matching types
a0 :: *
Eq Int :: Constraint
=====================================
testsuite/tests/typecheck/should_fail/T3950.stderr
=====================================
@@ -1,6 +1,6 @@
T3950.hs:16:13: error: [GHC-18872]
- • Couldn't match kind ‘* -> *’ with ‘*’
+ • Couldn't match kind ‘*’ with ‘* -> *’
When matching types
w :: (* -> * -> *) -> *
Sealed :: (* -> *) -> *
=====================================
testsuite/tests/typecheck/should_fail/T7368.stderr
=====================================
@@ -1,6 +1,6 @@
T7368.hs:3:10: error: [GHC-18872]
- • Couldn't match kind ‘*’ with ‘* -> *’
+ • Couldn't match kind ‘* -> *’ with ‘*’
When matching types
b0 :: *
Maybe :: * -> *
=====================================
testsuite/tests/typecheck/should_fail/T7368a.stderr
=====================================
@@ -1,6 +1,6 @@
T7368a.hs:8:6: error: [GHC-18872]
- • Couldn't match kind ‘*’ with ‘* -> *’
+ • Couldn't match kind ‘* -> *’ with ‘*’
When matching types
f :: * -> *
Bad :: (* -> *) -> *
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/9ab0c9d2e30e2e25f78e5dfa6f2f76e891c8dcfe...8e27d5409352d6c268d33d43c2b5c30fa42a2f43
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/9ab0c9d2e30e2e25f78e5dfa6f2f76e891c8dcfe...8e27d5409352d6c268d33d43c2b5c30fa42a2f43
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/20230412/84639cad/attachment-0001.html>
More information about the ghc-commits
mailing list