Can you implement `foo` without `coerce`?

Foo.hs

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
module Foo where

import Data.Coerce

type family F a
newtype T1 = MkT1 (forall a. F a)
newtype T2 = MkT2 (forall a. F a)

foo :: T1 -> T2
foo = coerce

{-
If you try this:

  foo :: T1 -> T2
  foo (MkT1 x) = MkT2 x
  
You get this:


[1 of 1] Compiling Foo              ( Bug.hs, interpreted )

Bug.hs:13:21: error:
    • Couldn't match expected type ‘F a’ with actual type ‘F a0’
      NB: ‘F’ is a non-injective type family
      The type variable ‘a0’ is ambiguous
    • In the first argument of ‘MkT2’, namely ‘x’
      In the expression: MkT2 x
      In an equation for ‘foo’: foo (MkT1 x) = MkT2 x
   |
13 | foo (MkT1 x) = MkT2 x
   |                     ^
-}