Possible bug in isReflexiveCo?
Perhaps I'm missing something, but isReflexiveCo_maybe
looks incorrect to me. Here's the definition:
isReflexiveCo_maybe :: Coercion -> Maybe (Type, Role)
isReflexiveCo_maybe (Refl ty) = Just (ty, Nominal)
isReflexiveCo_maybe (GRefl r ty mco) | isGReflMCo mco = Just (ty, r)
isReflexiveCo_maybe co
| ty1 `eqType` ty2
= Just (ty1, r)
| otherwise
= Nothing
where (Pair ty1 ty2, r) = coercionKindRole co
Note that the GRefl
case uses isGReflMCo
, which in turn calls isGReflCo
, doing a quick check for generalized reflexivity. Thus isReflexiveCo_maybe
will return Nothing
given GRefl r ty (MCo co)
if co
is reflexive but non-trivial, e.g. cv ; Sym cv
. Is there some reason this can't happen? Or does it make it possible to violate invariant (EQ2) using mkCastTy
?