Commit 2f9809ef authored by eir@cis.upenn.edu's avatar eir@cis.upenn.edu

Slightly better `Coercible` errors.

This makes two real changes:
 - Equalities like (a ~R [a]) really *are* insoluble. Previously,
   GHC refused to give up when an occurs check bit on a representational
   equality. But for datatypes, it really should bail.

 - Now, GHC will sometimes report an occurs check error (in cases above)
   for representational equalities. Previously, it never did.

This "fixes" #10715, where by "fix", I mean clarifies the error message.
It's unclear how to do more to fix that ticket.

Test cases: typecheck/should_fail/T10715{,b}
parent cbcad859
......@@ -1016,6 +1016,23 @@ and the Id newtype is unwrapped. This is assured by requiring only flat
types in canEqTyVar *and* having the newtype-unwrapping check above
the tyvar check in can_eq_nc.
Note [Occurs check error]
~~~~~~~~~~~~~~~~~~~~~~~~~
If we have an occurs check error, are we necessarily hosed? Say our
tyvar is tv1 and the type it appears in is xi2. Because xi2 is function
free, then if we're computing w.r.t. nominal equality, then, yes, we're
hosed. Nothing good can come from (a ~ [a]). If we're computing w.r.t.
representational equality, this is a little subtler. Once again, (a ~R [a])
is a bad thing, but (a ~R N a) for a newtype N might be just fine. This
means also that (a ~ b a) might be fine, because `b` might become a newtype.
So, we must check: does tv1 appear in xi2 under any type constructor that
is generative w.r.t. representational equality? That's what isTyVarUnderDatatype
does. (The other name I considered, isTyVarUnderTyConGenerativeWrtReprEq was
a bit verbose. And the shorter name gets the point across.)
See also #10715, which induced this addition.
-}
canCFunEqCan :: CtEvidence
......@@ -1091,12 +1108,14 @@ canEqTyVar2 dflags ev eq_rel swapped tv1 xi2
| otherwise -- Occurs check error
= rewriteEqEvidence ev eq_rel swapped xi1 xi2 co1 co2
`andWhenContinue` \ new_ev ->
case eq_rel of
NomEq -> do { emitInsoluble (mkNonCanonical new_ev)
if eq_rel == NomEq || isTyVarUnderDatatype tv1 xi2
-- See Note [Occurs check error]
then do { emitInsoluble (mkNonCanonical new_ev)
-- If we have a ~ [a], it is not canonical, and in particular
-- we don't want to rewrite existing inerts with it, otherwise
-- we'd risk divergence in the constraint solver
; stopWith new_ev "Occurs check" }
; stopWith new_ev "Occurs check" }
-- A representational equality with an occurs-check problem isn't
-- insoluble! For example:
......@@ -1104,9 +1123,9 @@ canEqTyVar2 dflags ev eq_rel swapped tv1 xi2
-- We might learn that b is the newtype Id.
-- But, the occurs-check certainly prevents the equality from being
-- canonical, and we might loop if we were to use it in rewriting.
ReprEq -> do { traceTcS "Occurs-check in representational equality"
else do { traceTcS "Occurs-check in representational equality"
(ppr xi1 $$ ppr xi2)
; continueWith (CIrredEvCan { cc_ev = new_ev }) }
; continueWith (CIrredEvCan { cc_ev = new_ev }) }
where
role = eqRelRole eq_rel
xi1 = mkTyVarTy tv1
......
......@@ -963,7 +963,10 @@ mkTyVarEqErr dflags ctxt extra ct oriented tv1 ty2
-- be oriented the other way round;
-- see TcCanonical.canEqTyVarTyVar
|| isSigTyVar tv1 && not (isTyVarTy ty2)
|| ctEqRel ct == ReprEq -- the cases below don't really apply to ReprEq
|| pprTrace "RAE1" (ppr ct $$ ppr tv1 $$ ppr ty2 $$
ppr (isTyVarUnderDatatype tv1 ty2))
(ctEqRel ct == ReprEq && not (isTyVarUnderDatatype tv1 ty2))
-- the cases below don't really apply to ReprEq (except occurs check)
= mkErrorMsgFromCt ctxt ct (vcat [ misMatchOrCND ctxt ct oriented ty1 ty2
, extraTyVarInfo ctxt tv1 ty2
, extra ])
......@@ -975,7 +978,8 @@ mkTyVarEqErr dflags ctxt extra ct oriented tv1 ty2
= mkErrorMsgFromCt ctxt ct $ (kindErrorMsg (mkTyVarTy tv1) ty2 $$ extra)
| OC_Occurs <- occ_check_expand
, NomEq <- ctEqRel ct -- reporting occurs check for Coercible is strange
, ctEqRel ct == NomEq || isTyVarUnderDatatype tv1 ty2
-- See Note [Occurs check error] in TcCanonical
= do { let occCheckMsg = addArising (ctOrigin ct) $
hang (text "Occurs check: cannot construct the infinite type:")
2 (sep [ppr ty1, char '~', ppr ty2])
......
......@@ -68,7 +68,7 @@ module TcType (
isDoubleTy, isFloatTy, isIntTy, isWordTy, isStringTy,
isIntegerTy, isBoolTy, isUnitTy, isCharTy,
isTauTy, isTauTyCon, tcIsTyVarTy, tcIsForAllTy,
isPredTy, isTyVarClassPred, isTyVarExposed,
isPredTy, isTyVarClassPred, isTyVarExposed, isTyVarUnderDatatype,
checkValidClsArgs, hasTyVarHead,
isRigidEqPred, isRigidTy,
......@@ -1466,6 +1466,25 @@ isTyVarExposed tv (AppTy fun arg) = isTyVarExposed tv fun
|| isTyVarExposed tv arg
isTyVarExposed _ (ForAllTy {}) = False
-- | Does the given tyvar appear under a type generative w.r.t.
-- representational equality? See Note [Occurs check error] in
-- TcCanonical for the motivation for this function.
isTyVarUnderDatatype :: TcTyVar -> TcType -> Bool
isTyVarUnderDatatype tv = go False
where
go under_dt ty | Just ty' <- tcView ty = go under_dt ty'
go under_dt (TyVarTy tv') = under_dt && (tv == tv')
go under_dt (TyConApp tc tys) = let under_dt' = under_dt ||
isGenerativeTyCon tc
Representational
in any (go under_dt') tys
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 tv' inner_ty)
| tv' == tv = False
| otherwise = go under_dt inner_ty
isRigidTy :: TcType -> Bool
isRigidTy ty
| Just (tc,_) <- tcSplitTyConApp_maybe ty = isGenerativeTyCon tc Nominal
......
{-# LANGUAGE FlexibleContexts #-}
module T10715 where
import Data.Coerce (coerce, Coercible)
import Data.Ord ( Down ) -- convenient newtype
data X a
doCoerce :: Coercible a (X a) => a -> X a
doCoerce = coerce
T10715.hs:9:13: error:
Couldn't match representation of type ‘a’ with that of ‘X a’
‘a’ is a rigid type variable bound by
the type signature for:
doCoerce :: Coercible a (X a) => a -> X a
at T10715.hs:9:13
Inaccessible code in
the type signature for:
doCoerce :: Coercible a (X a) => a -> X a
In the ambiguity check for the type signature for ‘doCoerce’:
doCoerce :: forall a. Coercible a (X a) => a -> X a
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
In the type signature for ‘doCoerce’:
doCoerce :: Coercible a (X a) => a -> X a
module T10715b where
-- test error message: should complain about an occurs check
import Data.Coerce
foo = coerce `asTypeOf` head
T10715b.hs:7:7: error:
Occurs check: cannot construct the infinite type: b ~ [b]
arising from a use of ‘coerce’
Relevant bindings include foo :: [b] -> b (bound at T10715b.hs:7:1)
In the first argument of ‘asTypeOf’, namely ‘coerce’
In the expression: coerce `asTypeOf` head
In an equation for ‘foo’: foo = coerce `asTypeOf` head
......@@ -386,3 +386,5 @@ 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', normal, compile_fail, [''])
test('T10715', normal, compile_fail, [''])
test('T10715b', 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