[Git][ghc/ghc][wip/T22194-flags] Wibbles
Simon Peyton Jones (@simonpj)
gitlab at gitlab.haskell.org
Wed Mar 22 15:45:57 UTC 2023
Simon Peyton Jones pushed to branch wip/T22194-flags at Glasgow Haskell Compiler / GHC
Commits:
554c9a5d by Simon Peyton Jones at 2023-03-22T15:47:14+00:00
Wibbles
- - - - -
7 changed files:
- compiler/GHC/Tc/Solver/Monad.hs
- compiler/GHC/Tc/Types/Constraint.hs
- compiler/GHC/Tc/Utils/Unify.hs
- testsuite/tests/partial-sigs/should_compile/T10403.stderr
- testsuite/tests/polykinds/T9017.stderr
- testsuite/tests/rep-poly/T13929.stderr
- testsuite/tests/typecheck/should_fail/T16512a.stderr
Changes:
=====================================
compiler/GHC/Tc/Solver/Monad.hs
=====================================
@@ -179,7 +179,7 @@ import GHC.Data.Bag as Bag
import GHC.Data.Pair
import GHC.Utils.Monad
-import GHC.Utils.Misc( equalLength )
+import GHC.Utils.Misc( equalLength, lengthIs )
import GHC.Exts (oneShot)
import Control.Monad
@@ -2091,8 +2091,13 @@ checkTouchableTyVarEq ev lhs_tv rhs
| Just (tc,tys) <- splitTyConApp_maybe rhs
, isTypeFamilyTyCon tc
, not (isConcreteTyVar lhs_tv)
- = do { tys_res <- mapCheck (checkTyEqRhs arg_flags) tys
- ; return (mkTyConAppRedn Nominal tc <$> tys_res) }
+ , let arity = tyConArity tc
+ = if tys `lengthIs` arity
+ then recurseIntoTyConApp arg_flags tc tys
+ else do { let (fun_args, extra_args) = splitAt (tyConArity tc) tys
+ ; fun_res <- recurseIntoTyConApp arg_flags tc fun_args
+ ; extra_res <- mapCheck (checkTyEqRhs flags) extra_args
+ ; return (mkAppRedns <$> fun_res <*> extra_res) }
| otherwise = checkTyEqRhs flags rhs
=====================================
compiler/GHC/Tc/Types/Constraint.hs
=====================================
@@ -590,23 +590,31 @@ instance Semigroup CheckTyEqResult where
instance Monoid CheckTyEqResult where
mempty = cteOK
+instance Eq CheckTyEqProblem where
+ (CTEP b1) == (CTEP b2) = b1==b2
+
+instance Outputable CheckTyEqProblem where
+ ppr prob@(CTEP bits) = case lookup prob allBits of
+ Just s -> text s
+ Nothing -> text "unknown:" <+> ppr bits
+
instance Outputable CheckTyEqResult where
ppr cter | cterHasNoProblem cter
= text "cteOK"
| otherwise
- = braces $ fcat $ intersperse vbar $ set_bits
- where
- all_bits = [ (cteImpredicative, "cteImpredicative")
- , (cteTypeFamily, "cteTypeFamily")
- , (cteInsolubleOccurs, "cteInsolubleOccurs")
- , (cteSolubleOccurs, "cteSolubleOccurs")
- , (cteConcrete, "cteConcrete")
- , (cteSkolemEscape, "cteSkolemEscape")
- , (cteCoercionHole, "cteCoercionHole")
- ]
- set_bits = [ text str
- | (bitmask, str) <- all_bits
- , cter `cterHasProblem` bitmask ]
+ = braces $ fcat $ intersperse vbar $
+ [ text str
+ | (bitmask, str) <- allBits
+ , cter `cterHasProblem` bitmask ]
+
+allBits :: [(CheckTyEqProblem, String)]
+allBits = [ (cteImpredicative, "cteImpredicative")
+ , (cteTypeFamily, "cteTypeFamily")
+ , (cteInsolubleOccurs, "cteInsolubleOccurs")
+ , (cteSolubleOccurs, "cteSolubleOccurs")
+ , (cteConcrete, "cteConcrete")
+ , (cteSkolemEscape, "cteSkolemEscape")
+ , (cteCoercionHole, "cteCoercionHole") ]
{- Note [CIrredCan constraints]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
=====================================
compiler/GHC/Tc/Utils/Unify.hs
=====================================
@@ -2,6 +2,7 @@
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE RecursiveDo #-}
{-# LANGUAGE MultiWayIf #-}
+{-# LANGUAGE RecordWildCards #-}
{-
(c) The University of Glasgow 2006
@@ -33,10 +34,10 @@ module GHC.Tc.Utils.Unify (
matchExpectedFunKind,
matchActualFunTySigma, matchActualFunTysRho,
- checkTyEqRhs,
+ checkTyEqRhs, recurseIntoTyConApp,
PuResult(..), failCheckWith, okCheckRefl, mapCheck,
TyEqFlags(..), TyEqFamApp(..), AreUnifying(..), LevelCheck(..), FamAppBreaker,
- famAppArgFlags, occursCheckTv, simpleUnifyCheck, checkPromoteFreeVars
+ famAppArgFlags, occursCheckTv, simpleUnifyCheck, checkPromoteFreeVars,
) where
import GHC.Prelude
@@ -2745,6 +2746,11 @@ instance (Outputable a, Outputable b) => Outputable (PuResult a b) where
(vcat [ text "redn:" <+> ppr x
, text "cts:" <+> ppr cts ])
+pprPur :: PuResult a b -> SDoc
+-- For debugging
+pprPur (PuFail prob) = text "PuFail:" <> ppr prob
+
+pprPur (PuOK {}) = text "PuOK"
okCheckRefl :: TcType -> TcM (PuResult a Reduction)
okCheckRefl ty = return (PuOK (mkReflRedn Nominal ty) emptyBag)
@@ -2797,6 +2803,29 @@ data LevelCheck
| LC_Promote -- Do a level check against this level; if it fails on a
-- unification variable, promote it
+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 ])
+
+instance Outputable (TyEqFamApp a) where
+ ppr TEFA_Fail = text "TEFA_Fail"
+ ppr TEFA_Recurse = text "TEFA_Fail"
+ ppr (TEFA_Break {}) = text "TEFA_Brefak"
+
+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 = text "LC_Promote"
+
famAppArgFlags :: TyEqFlags a -> TyEqFlags a
-- Adjust the flags when going undter a type family
-- Only the outer family application gets the loop-breaker treatment
@@ -2956,6 +2985,7 @@ checkTyConApp flags@(TEF { tef_unifying = unifying, tef_foralls = foralls_ok })
fun_app = mkTyConApp tc fun_args
; fun_res <- checkFamApp flags fun_app tc fun_args
; extra_res <- mapCheck (checkTyEqRhs flags) extra_args
+ ; traceTc "Over-sat" (ppr tc <+> ppr tys $$ ppr arity $$ pprPur fun_res $$ pprPur extra_res)
; return (mkAppRedns <$> fun_res <*> extra_res) }
| not (isFamFreeTyCon tc) || isForgetfulSynTyCon tc
@@ -2974,6 +3004,10 @@ checkTyConApp flags@(TEF { tef_unifying = unifying, tef_foralls = foralls_ok })
= failCheckWith (cteProblem cteConcrete)
| otherwise -- Recurse on arguments
+ = recurseIntoTyConApp flags tc tys
+
+recurseIntoTyConApp :: TyEqFlags a -> TyCon -> [TcType] -> TcM (PuResult a Reduction)
+recurseIntoTyConApp flags tc tys
= do { tys_res <- mapCheck (checkTyEqRhs flags) tys
; return (mkTyConAppRedn Nominal tc <$> tys_res) }
@@ -2990,7 +3024,7 @@ checkFamApp flags@(TEF { tef_unifying = unifying, tef_occurs = occ_prob
| otherwise
= case fam_app_flag of
- TEFA_Fail -> failCheckWith (cteProblem cteTypeFamily)
+ TEFA_Fail -> failCheckWith (cteProblem cteTypeFamily)
TEFA_Recurse
| TyFamLHS lhs_tc lhs_tys <- lhs
@@ -2999,6 +3033,7 @@ checkFamApp flags@(TEF { tef_unifying = unifying, tef_occurs = occ_prob
| otherwise
-> do { tys_res <- mapCheck (checkTyEqRhs arg_flags) tys
+ ; traceTc "under" (ppr tc $$ pprPur tys_res $$ ppr flags)
; return (mkTyConAppRedn Nominal tc <$> tys_res) }
TEFA_Break breaker
=====================================
testsuite/tests/partial-sigs/should_compile/T10403.stderr
=====================================
@@ -15,22 +15,39 @@ T10403.hs:16:12: warning: [GHC-88464] [-Wpartial-type-signatures (in -Wdefault)]
T10403.hs:20:7: warning: [GHC-88464] [-Wpartial-type-signatures (in -Wdefault)]
• Found type wildcard ‘_’
- standing for ‘(a1 -> a2) -> B t0 a1 -> H (B t0)’
- Where: ‘t0’ is an ambiguous type variable
+ standing for ‘(a1 -> a2) -> f0 a1 -> H f0’
+ Where: ‘f0’ is an ambiguous type variable
‘a2’, ‘a1’ are rigid type variables bound by
- the inferred type of h2 :: (a1 -> a2) -> B t0 a1 -> H (B t0)
+ the inferred type of h2 :: (a1 -> a2) -> f0 a1 -> H f0
at T10403.hs:23:1-41
• In the type signature: h2 :: _
+T10403.hs:23:15: warning: [GHC-39999] [-Wdeferred-type-errors (in -Wdefault)]
+ • Ambiguous type variable ‘f0’ arising from a use of ‘fmap’
+ prevents the constraint ‘(Functor f0)’ from being solved.
+ Relevant bindings include
+ b :: f0 a1 (bound at T10403.hs:23:6)
+ h2 :: (a1 -> a2) -> f0 a1 -> H f0 (bound at T10403.hs:23:1)
+ Probable fix: use a type annotation to specify what ‘f0’ should be.
+ Potentially matching instances:
+ instance Functor IO -- Defined in ‘GHC.Base’
+ instance Functor (B t) -- Defined at T10403.hs:11:10
+ ...plus 8 others
+ ...plus one instance involving out-of-scope types
+ (use -fprint-potential-instances to see them all)
+ • In the second argument of ‘(.)’, namely ‘fmap (const ())’
+ In the expression: (H . fmap (const ())) (fmap f b)
+ In an equation for ‘h2’: h2 f b = (H . fmap (const ())) (fmap f b)
+
T10403.hs:29:8: warning: [GHC-46956] [-Wdeferred-type-errors (in -Wdefault)]
- • Couldn't match type ‘t0’ with ‘t’
+ • Couldn't match type ‘f0’ with ‘B t’
Expected: H (B t)
- Actual: H (B t0)
- because type variable ‘t’ would escape its scope
- This (rigid, skolem) type variable is bound by
- the type signature for:
- app2 :: forall t. H (B t)
- at T10403.hs:28:1-15
+ Actual: H f0
+ • because type variable ‘t’ would escape its scope
+ This (rigid, skolem) type variable is bound by
+ the type signature for:
+ app2 :: forall t. H (B t)
+ at T10403.hs:28:1-15
• In the expression: h2 (H . I) (B ())
In an equation for ‘app2’: app2 = h2 (H . I) (B ())
• Relevant bindings include
=====================================
testsuite/tests/polykinds/T9017.stderr
=====================================
@@ -1,12 +1,12 @@
T9017.hs:8:7: error: [GHC-25897]
- • Couldn't match kind ‘k1’ with ‘*’
+ • Couldn't match kind ‘k2’ with ‘*’
When matching types
a0 :: * -> * -> *
a :: k1 -> k2 -> *
Expected: a b (m b)
Actual: a0 b0 (m0 b0)
- ‘k1’ is a rigid type variable bound by
+ ‘k2’ 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/rep-poly/T13929.stderr
=====================================
@@ -3,8 +3,8 @@ T13929.hs:29:24: error: [GHC-55287]
• The tuple argument in first position
does not have a fixed runtime representation.
Its type is:
- GUnboxed f LiftedRep :: TYPE c0
- Cannot unify ‘rf’ with the type variable ‘c0’
+ a0 :: TYPE k00
+ Cannot unify ‘rf’ with the type variable ‘k00’
because it is not a concrete ‘RuntimeRep’.
• In the expression: (# gunbox x, gunbox y #)
In an equation for ‘gunbox’:
@@ -12,7 +12,6 @@ T13929.hs:29:24: error: [GHC-55287]
In the instance declaration for
‘GUnbox (f :*: g) (TupleRep [rf, rg])’
• Relevant bindings include
- x :: f p (bound at T13929.hs:29:13)
gunbox :: (:*:) f g p -> GUnboxed (f :*: g) (TupleRep [rf, rg])
(bound at T13929.hs:29:5)
=====================================
testsuite/tests/typecheck/should_fail/T16512a.stderr
=====================================
@@ -1,18 +1,20 @@
T16512a.hs:41:25: error: [GHC-25897]
- • Couldn't match type ‘b’ with ‘a -> b’
+ • Couldn't match type ‘as’ with ‘a : as’
Expected: AST (ListVariadic (a : as) b)
Actual: AST (ListVariadic as (a -> b))
- ‘b’ is a rigid type variable bound by
- the type signature for:
- unapply :: forall b. AST b -> AnApplication b
- at T16512a.hs:37:1-35
+ ‘as’ is a rigid type variable bound by
+ a pattern with constructor:
+ AnApplication :: forall (as :: [*]) b.
+ AST (ListVariadic as b) -> ASTs as -> AnApplication b,
+ in a case alternative
+ at T16512a.hs:40:9-26
• In the first argument of ‘AnApplication’, namely ‘g’
In the expression: AnApplication g (a `ConsAST` as)
In a case alternative:
AnApplication g as -> AnApplication g (a `ConsAST` as)
• Relevant bindings include
+ as :: ASTs as (bound at T16512a.hs:40:25)
g :: AST (ListVariadic as (a -> b)) (bound at T16512a.hs:40:23)
a :: AST a (bound at T16512a.hs:38:15)
f :: AST (a -> b) (bound at T16512a.hs:38:10)
- unapply :: AST b -> AnApplication b (bound at T16512a.hs:38:1)
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/554c9a5df5374f3c9c4253c69e98e08dacf20870
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/554c9a5df5374f3c9c4253c69e98e08dacf20870
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/20230322/8f08e2fe/attachment-0001.html>
More information about the ghc-commits
mailing list