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?