Commit e71976a7 authored by's avatar Committed by Ben Gamari
Browse files

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 b13c6fe9
......@@ -926,6 +926,23 @@ of can_eq_nc. We know that this can't loop forever because we require that
flattening the RHS actually made progress. (If it didn't, then we really
*should* fail with an occurs-check!)
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
......@@ -1032,12 +1049,14 @@ canEqTyVar2 dflags ev eq_rel swapped tv1 xi2 co2
| 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:
......@@ -1045,9 +1064,9 @@ canEqTyVar2 dflags ev eq_rel swapped tv1 xi2 co2
-- 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 }) }
xi1 = mkTyVarTy tv1
co1 = mkTcReflCo (eqRelRole eq_rel) xi1
......@@ -815,7 +815,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)
= mkErrorMsg ctxt ct (vcat [ misMatchOrCND ctxt ct oriented ty1 ty2
, extraTyVarInfo ctxt tv1 ty2
, extra ])
......@@ -827,7 +830,8 @@ mkTyVarEqErr dflags ctxt extra ct oriented tv1 ty2
= mkErrorMsg 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 = hang (text "Occurs check: cannot construct the infinite type:")
2 (sep [ppr ty1, char '~', ppr ty2])
extra2 = mkEqInfoMsg ct ty1 ty2
......@@ -68,7 +68,7 @@ module TcType (
isFloatingTy, isDoubleTy, isFloatTy, isIntTy, isWordTy, isStringTy,
isIntegerTy, isBoolTy, isUnitTy, isCharTy,
isTauTy, isTauTyCon, tcIsTyVarTy, tcIsForAllTy,
isPredTy, isTyVarClassPred, isTyVarExposed,
isPredTy, isTyVarClassPred, isTyVarExposed, isTyVarUnderDatatype,
-- Misc type manipulators
......@@ -1432,6 +1432,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
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
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
* *
{-# 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
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
Occurs check: cannot construct the infinite type: b ~ [b]
Relevant role signatures: type role [] representational
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
......@@ -364,3 +364,5 @@ test('T9858e', normal, compile_fail, [''])
test('T10534', extra_clean(['T10534a.hi', 'T10534a.o']),
multimod_compile_fail, ['T10534', '-v0'])
test('T10495', 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