Commit e0ad55f8 authored by Simon Peyton Jones's avatar Simon Peyton Jones
Browse files

Fix error-message suppress on given equalities

I'd got the logic slightly wrong when reporting type errors
for insoluble 'given' equalities.  We suppress insoluble givens
under some circumstances (see Note [Given errors]), but we then
suppressed subsequent 'wanted' errors because the (suppressed)
'given' error "won".  Result: no errors at all :-(.

This patch fixes it and
 - Renames TcType.isTyVarUnderDatatype to the more
   perspicuous TcType.isInsolubleOccursCheck

In doing this I realise that I don't understand why we need
to keep the insolubles partitioned out separately at all...
but that is for another day.
parent 7c7479d0
...@@ -1439,11 +1439,12 @@ canEqTyVar2 dflags ev eq_rel swapped tv1 xi2 ...@@ -1439,11 +1439,12 @@ canEqTyVar2 dflags ev eq_rel swapped tv1 xi2
CTyEqCan { cc_ev = new_new_ev, cc_tyvar = tv1 CTyEqCan { cc_ev = new_new_ev, cc_tyvar = tv1
, cc_rhs = xi2'', cc_eq_rel = eq_rel } , cc_rhs = xi2'', cc_eq_rel = eq_rel }
| otherwise -- Occurs check error (or a forall) | otherwise -- For some reason (occurs check, or forall) we can't unify
= do { traceTcS "canEqTyVar2 occurs check error" (ppr tv1 $$ ppr xi2) -- We must not use it for further rewriting!
= do { traceTcS "canEqTyVar2 can't unify" (ppr tv1 $$ ppr xi2)
; rewriteEqEvidence ev swapped xi1 xi2 co1 co2 ; rewriteEqEvidence ev swapped xi1 xi2 co1 co2
`andWhenContinue` \ new_ev -> `andWhenContinue` \ new_ev ->
if eq_rel == NomEq || isTyVarUnderDatatype tv1 xi2 if isInsolubleOccursCheck eq_rel tv1 xi2
then do { emitInsoluble (mkNonCanonical new_ev) then do { emitInsoluble (mkNonCanonical new_ev)
-- If we have a ~ [a], it is not canonical, and in particular -- If we have a ~ [a], it is not canonical, and in particular
-- we don't want to rewrite existing inerts with it, otherwise -- we don't want to rewrite existing inerts with it, otherwise
...@@ -1456,7 +1457,7 @@ canEqTyVar2 dflags ev eq_rel swapped tv1 xi2 ...@@ -1456,7 +1457,7 @@ canEqTyVar2 dflags ev eq_rel swapped tv1 xi2
-- We might learn that b is the newtype Id. -- We might learn that b is the newtype Id.
-- But, the occurs-check certainly prevents the equality from being -- But, the occurs-check certainly prevents the equality from being
-- canonical, and we might loop if we were to use it in rewriting. -- canonical, and we might loop if we were to use it in rewriting.
else do { traceTcS "Occurs-check in representational equality" else do { traceTcS "Possibly-soluble occurs check"
(ppr xi1 $$ ppr xi2) (ppr xi1 $$ ppr xi2)
; continueWith (CIrredEvCan { cc_ev = new_ev }) } } ; continueWith (CIrredEvCan { cc_ev = new_ev }) } }
where where
......
...@@ -308,6 +308,25 @@ data ReportErrCtxt ...@@ -308,6 +308,25 @@ data ReportErrCtxt
-- See Note [Suppressing error messages] -- See Note [Suppressing error messages]
} }
instance Outputable ReportErrCtxt where
ppr (CEC { cec_binds = bvar
, cec_errors_as_warns = ew
, cec_defer_type_errors = dte
, cec_expr_holes = eh
, cec_type_holes = th
, cec_out_of_scope_holes = osh
, cec_warn_redundant = wr
, cec_suppress = sup })
= text "CEC" <+> braces (vcat
[ text "cec_binds" <+> equals <+> ppr bvar
, text "cec_errors_as_warns" <+> equals <+> ppr ew
, text "cec_defer_type_errors" <+> equals <+> ppr dte
, text "cec_expr_holes" <+> equals <+> ppr eh
, text "cec_type_holes" <+> equals <+> ppr th
, text "cec_out_of_scope_holes" <+> equals <+> ppr osh
, text "cec_warn_redundant" <+> equals <+> ppr wr
, text "cec_suppress" <+> equals <+> ppr sup ])
{- {-
Note [Suppressing error messages] Note [Suppressing error messages]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
...@@ -411,13 +430,14 @@ This only matters in instance declarations.. ...@@ -411,13 +430,14 @@ This only matters in instance declarations..
reportWanteds :: ReportErrCtxt -> TcLevel -> WantedConstraints -> TcM () reportWanteds :: ReportErrCtxt -> TcLevel -> WantedConstraints -> TcM ()
reportWanteds ctxt tc_lvl (WC { wc_simple = simples, wc_insol = insols, wc_impl = implics }) reportWanteds ctxt tc_lvl (WC { wc_simple = simples, wc_insol = insols, wc_impl = implics })
= do { traceTc "reportWanteds" (vcat [ text "Simples =" <+> ppr simples = do { traceTc "reportWanteds" (vcat [ text "Simples =" <+> ppr simples
, text "Insols =" <+> ppr insols
, text "Suppress =" <+> ppr (cec_suppress ctxt)]) , text "Suppress =" <+> ppr (cec_suppress ctxt)])
; let tidy_cts = bagToList (mapBag (tidyCt env) (insols `unionBags` simples)) ; let tidy_cts = bagToList (mapBag (tidyCt env) (insols `unionBags` simples))
-- First deal with things that are utterly wrong -- First deal with things that are utterly wrong
-- Like Int ~ Bool (incl nullary TyCons) -- Like Int ~ Bool (incl nullary TyCons)
-- or Int ~ t a (AppTy on one side) -- or Int ~ t a (AppTy on one side)
-- These ones are not suppressed by the incoming context -- These /ones/ are not suppressed by the incoming context
; let ctxt_for_insols = ctxt { cec_suppress = False } ; let ctxt_for_insols = ctxt { cec_suppress = False }
; (ctxt1, cts1) <- tryReporters ctxt_for_insols report1 tidy_cts ; (ctxt1, cts1) <- tryReporters ctxt_for_insols report1 tidy_cts
...@@ -448,7 +468,7 @@ reportWanteds ctxt tc_lvl (WC { wc_simple = simples, wc_insol = insols, wc_impl ...@@ -448,7 +468,7 @@ reportWanteds ctxt tc_lvl (WC { wc_simple = simples, wc_insol = insols, wc_impl
-- type checking to get a Lint error later -- type checking to get a Lint error later
report1 = [ ("custom_error", is_user_type_error, report1 = [ ("custom_error", is_user_type_error,
True, mkUserTypeErrorReporter) True, mkUserTypeErrorReporter)
, ("insoluble1", is_given_eq, True, mkGivenErrorReporter) , given_eq_spec
, ("insoluble2", utterly_wrong, True, mkGroupReporter mkEqErr) , ("insoluble2", utterly_wrong, True, mkGroupReporter mkEqErr)
, ("skolem eq1", very_wrong, True, mkSkolReporter) , ("skolem eq1", very_wrong, True, mkSkolReporter)
, ("skolem eq2", skolem_eq, True, mkSkolReporter) , ("skolem eq2", skolem_eq, True, mkSkolReporter)
...@@ -490,12 +510,6 @@ reportWanteds ctxt tc_lvl (WC { wc_simple = simples, wc_insol = insols, wc_impl ...@@ -490,12 +510,6 @@ reportWanteds ctxt tc_lvl (WC { wc_simple = simples, wc_insol = insols, wc_impl
non_tv_eq _ (EqPred NomEq ty1 _) = not (isTyVarTy ty1) non_tv_eq _ (EqPred NomEq ty1 _) = not (isTyVarTy ty1)
non_tv_eq _ _ = False non_tv_eq _ _ = False
-- rigid_nom_eq _ pred = isRigidEqPred tc_lvl pred
--
-- rigid_nom_tv_eq _ pred
-- | EqPred _ ty1 _ <- pred = isRigidEqPred tc_lvl pred && isTyVarTy ty1
-- | otherwise = False
is_out_of_scope ct _ = isOutOfScopeCt ct is_out_of_scope ct _ = isOutOfScopeCt ct
is_hole ct _ = isHoleCt ct is_hole ct _ = isHoleCt ct
...@@ -513,6 +527,22 @@ reportWanteds ctxt tc_lvl (WC { wc_simple = simples, wc_insol = insols, wc_impl ...@@ -513,6 +527,22 @@ reportWanteds ctxt tc_lvl (WC { wc_simple = simples, wc_insol = insols, wc_impl
is_irred _ (IrredPred {}) = True is_irred _ (IrredPred {}) = True
is_irred _ _ = False is_irred _ _ = False
given_eq_spec = case find_gadt_match (cec_encl ctxt) of
Just imp -> ("insoluble1a", is_given_eq, True, mkGivenErrorReporter imp)
Nothing -> ("insoluble1b", is_given_eq, False, ignoreErrorReporter)
-- False means don't suppress subsequent errors
-- Reason: we don't report all given errors
-- (see mkGivenErrorReporter), and we should only suppress
-- subsequent errors if we actually report this one!
-- Trac #13446 is an example
find_gadt_match [] = Nothing
find_gadt_match (implic : implics)
| PatSkol {} <- ic_info implic
, not (ic_no_eqs implic)
= Just implic
| otherwise
= find_gadt_match implics
--------------- ---------------
isSkolemTy :: TcLevel -> Type -> Bool isSkolemTy :: TcLevel -> Type -> Bool
...@@ -580,10 +610,9 @@ mkUserTypeError ctxt ct = mkErrorMsgFromCt ctxt ct ...@@ -580,10 +610,9 @@ mkUserTypeError ctxt ct = mkErrorMsgFromCt ctxt ct
Nothing -> pprPanic "mkUserTypeError" (ppr ct) Nothing -> pprPanic "mkUserTypeError" (ppr ct)
mkGivenErrorReporter :: Reporter mkGivenErrorReporter :: Implication -> Reporter
-- See Note [Given errors] -- See Note [Given errors]
mkGivenErrorReporter ctxt cts mkGivenErrorReporter implic ctxt cts
| Just implic <- find_gadt_match (cec_encl ctxt)
= do { (ctxt, binds_msg, ct) <- relevantBindings True ctxt ct = do { (ctxt, binds_msg, ct) <- relevantBindings True ctxt ct
; dflags <- getDynFlags ; dflags <- getDynFlags
; let ct' = setCtLoc ct (setCtLocEnv (ctLoc ct) (ic_env implic)) ; let ct' = setCtLoc ct (setCtLocEnv (ctLoc ct) (ic_env implic))
...@@ -600,22 +629,17 @@ mkGivenErrorReporter ctxt cts ...@@ -600,22 +629,17 @@ mkGivenErrorReporter ctxt cts
; traceTc "mkGivenErrorRporter" (ppr ct) ; traceTc "mkGivenErrorRporter" (ppr ct)
; maybeReportError ctxt err } ; maybeReportError ctxt err }
| otherwise -- Discard Given errors that don't come from
-- a pattern match; maybe we should warn instead?
= do { traceTc "mkGivenErrorRporter no" (ppr ct $$ ppr (cec_encl ctxt))
; return () }
where where
(ct : _ ) = cts -- Never empty (ct : _ ) = cts -- Never empty
(ty1, ty2) = getEqPredTys (ctPred ct) (ty1, ty2) = getEqPredTys (ctPred ct)
find_gadt_match [] = Nothing ignoreErrorReporter :: Reporter
find_gadt_match (implic : implics) -- Discard Given errors that don't come from
| PatSkol {} <- ic_info implic -- a pattern match; maybe we should warn instead?ignoreErrorReporter ctxt cts
, not (ic_no_eqs implic) ignoreErrorReporter ctxt cts
= Just implic = do { traceTc "mkGivenErrorRporter no" (ppr cts $$ ppr (cec_encl ctxt))
| otherwise ; return () }
= find_gadt_match implics
{- Note [Given errors] {- Note [Given errors]
~~~~~~~~~~~~~~~~~~~~~~ ~~~~~~~~~~~~~~~~~~~~~~
...@@ -1442,7 +1466,7 @@ mkTyVarEqErr dflags ctxt report ct oriented tv1 ty2 ...@@ -1442,7 +1466,7 @@ mkTyVarEqErr dflags ctxt report ct oriented tv1 ty2
-- be oriented the other way round; -- be oriented the other way round;
-- see TcCanonical.canEqTyVarTyVar -- see TcCanonical.canEqTyVarTyVar
|| isSigTyVar tv1 && not (isTyVarTy ty2) || isSigTyVar tv1 && not (isTyVarTy ty2)
|| ctEqRel ct == ReprEq && not (isTyVarUnderDatatype tv1 ty2) || ctEqRel ct == ReprEq && not insoluble_occurs_check
-- the cases below don't really apply to ReprEq (except occurs check) -- the cases below don't really apply to ReprEq (except occurs check)
= mkErrorMsgFromCt ctxt ct $ mconcat = mkErrorMsgFromCt ctxt ct $ mconcat
[ important $ misMatchOrCND ctxt ct oriented ty1 ty2 [ important $ misMatchOrCND ctxt ct oriented ty1 ty2
...@@ -1454,7 +1478,7 @@ mkTyVarEqErr dflags ctxt report ct oriented tv1 ty2 ...@@ -1454,7 +1478,7 @@ mkTyVarEqErr dflags ctxt report ct oriented tv1 ty2
-- generalised it). So presumably it is an *untouchable* -- generalised it). So presumably it is an *untouchable*
-- meta tyvar or a SigTv, else it'd have been unified -- meta tyvar or a SigTv, else it'd have been unified
| OC_Occurs <- occ_check_expand | OC_Occurs <- occ_check_expand
, ctEqRel ct == NomEq || isTyVarUnderDatatype tv1 ty2 , insoluble_occurs_check
-- See Note [Occurs check error] in TcCanonical -- See Note [Occurs check error] in TcCanonical
= do { let occCheckMsg = important $ addArising (ctOrigin ct) $ = do { let occCheckMsg = important $ addArising (ctOrigin ct) $
hang (text "Occurs check: cannot construct the infinite" <+> what <> colon) hang (text "Occurs check: cannot construct the infinite" <+> what <> colon)
...@@ -1547,7 +1571,8 @@ mkTyVarEqErr dflags ctxt report ct oriented tv1 ty2 ...@@ -1547,7 +1571,8 @@ mkTyVarEqErr dflags ctxt report ct oriented tv1 ty2
-- Not an occurs check, because F is a type function. -- Not an occurs check, because F is a type function.
where where
ty1 = mkTyVarTy tv1 ty1 = mkTyVarTy tv1
occ_check_expand = occCheckForErrors dflags tv1 ty2 occ_check_expand = occCheckForErrors dflags tv1 ty2
insoluble_occurs_check = isInsolubleOccursCheck (ctEqRel ct) tv1 ty2
what = case ctLocTypeOrKind_maybe (ctLoc ct) of what = case ctLocTypeOrKind_maybe (ctLoc ct) of
Just KindLevel -> text "kind" Just KindLevel -> text "kind"
......
...@@ -78,7 +78,7 @@ module TcType ( ...@@ -78,7 +78,7 @@ module TcType (
isFloatingTy, isDoubleTy, isFloatTy, isIntTy, isWordTy, isStringTy, isFloatingTy, isDoubleTy, isFloatTy, isIntTy, isWordTy, isStringTy,
isIntegerTy, isBoolTy, isUnitTy, isCharTy, isCallStackTy, isCallStackPred, isIntegerTy, isBoolTy, isUnitTy, isCharTy, isCallStackTy, isCallStackPred,
isTauTy, isTauTyCon, tcIsTyVarTy, tcIsForAllTy, isTauTy, isTauTyCon, tcIsTyVarTy, tcIsForAllTy,
isPredTy, isTyVarClassPred, isTyVarExposed, isTyVarUnderDatatype, isPredTy, isTyVarClassPred, isTyVarExposed, isInsolubleOccursCheck,
checkValidClsArgs, hasTyVarHead, checkValidClsArgs, hasTyVarHead,
isRigidEqPred, isRigidTy, isRigidEqPred, isRigidTy,
...@@ -2149,26 +2149,35 @@ isTyVarExposed _ (FunTy {}) = False ...@@ -2149,26 +2149,35 @@ isTyVarExposed _ (FunTy {}) = False
isTyVarExposed tv (CastTy ty _) = isTyVarExposed tv ty isTyVarExposed tv (CastTy ty _) = isTyVarExposed tv ty
isTyVarExposed _ (CoercionTy {}) = False isTyVarExposed _ (CoercionTy {}) = False
-- | Does the given tyvar appear under a type generative w.r.t. -- | Is the equality
-- representational equality? See Note [Occurs check error] in -- a ~r ...a....
-- definitely insoluble or not?
-- a ~r Maybe a -- Definitely insoluble
-- a ~N ...(F a)... -- Not definitely insoluble
-- -- Perhaps (F a) reduces to Int
-- a ~R ...(N a)... -- Not definitely insoluble
-- -- Perhaps newtype N a = MkN Int
-- See Note [Occurs check error] in
-- TcCanonical for the motivation for this function. -- TcCanonical for the motivation for this function.
isTyVarUnderDatatype :: TcTyVar -> TcType -> Bool isInsolubleOccursCheck :: EqRel -> TcTyVar -> TcType -> Bool
isTyVarUnderDatatype tv = go False isInsolubleOccursCheck eq_rel tv ty
= go ty
where where
go under_dt ty | Just ty' <- coreView ty = go under_dt ty' go ty | Just ty' <- coreView ty = go ty'
go under_dt (TyVarTy tv') = under_dt && (tv == tv') go (TyVarTy tv') = tv == tv' || go (tyVarKind tv')
go under_dt (TyConApp tc tys) = let under_dt' = under_dt || go (LitTy {}) = False
isGenerativeTyCon tc go (AppTy t1 t2) = go t1 || go t2
Representational go (FunTy t1 t2) = go t1 || go t2
in any (go under_dt') tys go (ForAllTy (TvBndr tv' _) inner_ty)
go _ (LitTy {}) = False
go _ (FunTy arg res) = go True arg || go True res
go under_dt (AppTy fun arg) = go under_dt fun || go under_dt arg
go under_dt (ForAllTy (TvBndr tv' _) inner_ty)
| tv' == tv = False | tv' == tv = False
| otherwise = go under_dt inner_ty | otherwise = go (tyVarKind tv') || go inner_ty
go under_dt (CastTy ty _) = go under_dt ty go (CastTy ty _) = go ty -- ToDo: what about the coercion
go _ (CoercionTy {}) = False go (CoercionTy _) = False -- ToDo: what about the coercion
go (TyConApp tc tys)
| isGenerativeTyCon tc role = any go tys
| otherwise = False
role = eqRelRole eq_rel
isRigidTy :: TcType -> Bool isRigidTy :: TcType -> Bool
isRigidTy ty isRigidTy ty
......
...@@ -84,6 +84,11 @@ Defer01.hs:43:10: warning: [-Wdeferred-type-errors (in -Wdefault)] ...@@ -84,6 +84,11 @@ Defer01.hs:43:10: warning: [-Wdeferred-type-errors (in -Wdefault)]
In the expression: myOp 23 In the expression: myOp 23
In an equation for ‘j’: j = myOp 23 In an equation for ‘j’: j = myOp 23
Defer01.hs:47:7: warning: [-Wdeferred-type-errors (in -Wdefault)]
• Couldn't match expected type ‘Bool’ with actual type ‘Int’
• In the expression: x
In an equation for ‘k’: k x = x
Defer01.hs:50:5: warning: [-Wdeferred-type-errors (in -Wdefault)] Defer01.hs:50:5: warning: [-Wdeferred-type-errors (in -Wdefault)]
• Couldn't match expected type ‘IO a0’ • Couldn't match expected type ‘IO a0’
with actual type ‘Char -> IO ()’ with actual type ‘Char -> IO ()’
......
T2627b.hs:20:24: error: T2627b.hs:20:24: error:
• Occurs check: cannot construct the infinite type: • Couldn't match type ‘b0’ with ‘Dual (Dual b0)’
b0 ~ Dual (Dual b0)
arising from a use of ‘conn’ arising from a use of ‘conn’
The type variable ‘b0’ is ambiguous ‘b0’ is untouchable
inside the constraints: b ~ W e f
bound by a pattern with constructor:
Wr :: forall e f. e -> Comm f -> Comm (W e f),
in an equation for ‘conn’
at T2627b.hs:20:14-19
• In the expression: conn undefined undefined • In the expression: conn undefined undefined
In an equation for ‘conn’: In an equation for ‘conn’:
conn (Rd k) (Wr a r) = conn undefined undefined conn (Rd k) (Wr a r) = conn undefined undefined
T5934.hs:12:7: error: T5934.hs:12:7: error:
• Couldn't match expected type ‘(forall s. GenST s) -> Int’ • Cannot instantiate unification variable ‘a0’
with actual type ‘Integer’ with a type involving foralls: (forall s. GenST s) -> Int
GHC doesn't yet support impredicative polymorphism
• In the expression: 0
In an equation for ‘run’: run = 0
T5934.hs:12:7: error:
• Ambiguous type variable ‘a0’ arising from the literal ‘0’
prevents the constraint ‘(Num a0)’ from being solved.
Probable fix: use a type annotation to specify what ‘a0’ should be.
These potential instances exist:
instance Num Integer -- Defined in ‘GHC.Num’
instance Num Double -- Defined in ‘GHC.Float’
instance Num Float -- Defined in ‘GHC.Float’
...plus two others
(use -fprint-potential-instances to see them all)
• In the expression: 0 • In the expression: 0
In an equation for ‘run’: run = 0 In an equation for ‘run’: run = 0
T6123.hs:10:14: error: T6123.hs:10:14: error:
• Occurs check: cannot construct the infinite type: a0 ~ Id a0 • Couldn't match type ‘a0’ with ‘Id a0’ arising from a use of ‘cid’
arising from a use of ‘cid’
The type variable ‘a0’ is ambiguous The type variable ‘a0’ is ambiguous
• In the expression: cid undefined • In the expression: cid undefined
In an equation for ‘cundefined’: cundefined = cid undefined In an equation for ‘cundefined’: cundefined = cid undefined
......
T7354.hs:28:11: error: T7354.hs:28:11: error:
• Occurs check: cannot construct the infinite type: • Couldn't match type ‘p’ with ‘Base t (Prim [p] p)’
p ~ Base t (Prim [p] p) ‘p’ is a rigid type variable bound by
the inferred type of foo :: Prim [p] p -> t at T7354.hs:28:1-13
Expected type: Prim [p] p -> Base t (Prim [p] p) Expected type: Prim [p] p -> Base t (Prim [p] p)
Actual type: Prim [p] p -> p Actual type: Prim [p] p -> p
• In the first argument of ‘ana’, namely ‘alg’ • In the first argument of ‘ana’, namely ‘alg’
......
...@@ -2,15 +2,8 @@ ...@@ -2,15 +2,8 @@
T12427a.hs:17:29: error: T12427a.hs:17:29: error:
• Couldn't match expected type ‘p’ • Couldn't match expected type ‘p’
with actual type ‘(forall b. [b] -> [b]) -> Int’ with actual type ‘(forall b. [b] -> [b]) -> Int’
‘p’ is untouchable
inside the constraints: ()
bound by a pattern with constructor:
T1 :: forall a. a -> ((forall b. [b] -> [b]) -> Int) -> T,
in a case alternative
at T12427a.hs:17:19-24
‘p’ is a rigid type variable bound by ‘p’ is a rigid type variable bound by
the inferred type of h11 :: T -> p at T12427a.hs:17:1-29 the inferred type of h11 :: T -> p at T12427a.hs:17:1-29
Possible fix: add a type signature for ‘h11’
• In the expression: v • In the expression: v
In a case alternative: T1 _ v -> v In a case alternative: T1 _ v -> v
In the expression: case y of { T1 _ v -> v } In the expression: case y of { T1 _ v -> v }
...@@ -18,16 +11,8 @@ T12427a.hs:17:29: error: ...@@ -18,16 +11,8 @@ T12427a.hs:17:29: error:
h11 :: T -> p (bound at T12427a.hs:17:1) h11 :: T -> p (bound at T12427a.hs:17:1)
T12427a.hs:28:6: error: T12427a.hs:28:6: error:
• Couldn't match expected type ‘p’ • Cannot instantiate unification variable ‘p0’
with actual type ‘(forall b. [b] -> [b]) -> Int’ with a type involving foralls: (forall b. [b] -> [b]) -> Int
‘p’ is untouchable GHC doesn't yet support impredicative polymorphism
inside the constraints: ()
bound by a pattern with constructor:
T1 :: forall a. a -> ((forall b. [b] -> [b]) -> Int) -> T,
in a pattern binding
at T12427a.hs:28:1-7
‘p’ is a rigid type variable bound by
the inferred type of x1 :: p at T12427a.hs:28:1-19
Possible fix: add a type signature for ‘x1’
• In the pattern: T1 _ x1 • In the pattern: T1 _ x1
In a pattern binding: T1 _ x1 = undefined In a pattern binding: T1 _ x1 = undefined
T12589.hs:13:3: error: Variable not in scope: (&) :: t0 -> t1 -> t T12589.hs:13:3: error: Variable not in scope: (&) :: t0 -> t1 -> t
T12589.hs:13:5: error:
• Cannot instantiate unification variable ‘t1’
with a type involving foralls:
(forall a. Bounded a => f0 a) -> h0 f0 xs0
GHC doesn't yet support impredicative polymorphism
• In the second argument of ‘(&)’, namely ‘hcpure (Proxy @Bounded)’
In the expression: (&) minBound hcpure (Proxy @Bounded)
In an equation for ‘a’: a = (&) minBound hcpure (Proxy @Bounded)
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{- # OPTIONS_GHC -fno-defer-type-errors #-}
module T13446 where
import Data.Coerce (Coercible)
import GHC.Exts (Constraint)
import GHC.TypeLits (Symbol)
data Dict :: Constraint -> * where
Dict :: a => Dict a
infixr 9 :-
newtype a :- b = Sub (a => Dict b)
instance a => Show (a :- b) where
showsPrec d (Sub Dict) = showParen (d > 10) $ showString "Sub Dict"
class Lifting p f where
lifting :: p a :- p (f a)
data Blah a = Blah
newtype J (a :: JType) = J (Blah (J a))
newtype JComparable a = JComparable (J (T (JTy a)))
instance Lifting JReference JComparable where
lifting = Sub 'a'
class (Coercible a (J (JTy a))) => JReference a where
type JTy a :: JType
type T a
= 'Generic ('Iface "java.lang.Comparable") '[a]
data JType = Class Symbol
| Generic JType [JType]
| Iface Symbol
type JObject = J (Class "java.lang.Object")
instance JReference JObject where
type JTy JObject = 'Class "java.lang.Object"
T13446.hs:34:17: error:
• Couldn't match expected type ‘Dict (JReference (JComparable a))’
with actual type ‘Char’
• In the first argument of ‘Sub’, namely ‘'a'’
In the expression: Sub 'a'
In an equation for ‘lifting’: lifting = Sub 'a'
• Relevant bindings include
lifting :: JReference a :- JReference (JComparable a)
(bound at T13446.hs:34:3)
...@@ -430,3 +430,4 @@ test('LevPolyBounded', normal, compile_fail, ['']) ...@@ -430,3 +430,4 @@ test('LevPolyBounded', normal, compile_fail, [''])
test('T13292', normal, multimod_compile, ['T13292', '-v0 -fdefer-type-errors']) test('T13292', normal, multimod_compile, ['T13292', '-v0 -fdefer-type-errors'])
test('T13300', normal, compile_fail, ['']) test('T13300', normal, compile_fail, [''])
test('T12709', normal, compile_fail, ['']) test('T12709', normal, compile_fail, [''])
test('T13446', normal, compile_fail, [''])
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment