Inaccessible code might be accessible with newtypes and Coercible

If I say

module A (Age, ageCo) where

import Data.Type.Coercion

newtype Age = MkAge Int

ageCo :: Coercion Age Int
ageCo = Coercion

{-# LANGUAGE FlexibleContexts #-}

module B where

import Data.Coerce
import A

foo :: Coercible Age Int => ()
foo = ()

I get

B.hs:8:8: error:
    Couldn't match representation of type ‘Age’ with that of ‘Int’
    Inaccessible code in
      the type signature for: foo :: Coercible Age Int => ()
    In the ambiguity check for the type signature for ‘foo’:
      foo :: Coercible Age Int => ()
    To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
    In the type signature for ‘foo’: foo :: Coercible Age Int => ()

I agree that module B can't directly prove Coercible Age Int. But ageCo is in scope which proves exactly this! So it is provable, albeit indirectly. GHC should not claim that the code is inaccessible.

Proposed fix: in canDecomposableTyConApp, only call canEqHardFailure for a representational equality when both tycons involved say True to isDistinctTyCon.

I'm happy to put the fix in, once someone seconds this idea. Getting this right has proved harder than I thought!