need_prf.idr

record Foo where
  constructor MkFoo
  from : Type
  to : Type

bar : (a : Foo) -> (x : from a) -> (to a)
-- impl not important

baz : (a : Foo) -> (b : Foo) -> ((to b) = (from a)) => (x: from b) -> (to a)
baz a b x = do
  let y = bar b x
  -- ?hole
  let z = bar a y
  z

{-
When checking argument x to Main.bar:
        Type mismatch between
                to b (Type of y)
        and
                from a (Expected type)
-}

{-
a : Foo
b : Foo
x : from b
constraint : to b = from a
y : to b
--------------------------------------
hole : to a
-}

baz : (a : Foo) -> (b : Foo) -> a = b -> Foo.to b = Foo.from a -> (x : from b) -> to a
baz a b prf1 prf2 x =
  let y = bar b x
  in bar a (rewrite sym prf2 in y)

foo1 : Foo
foo1 = MkFoo String Nat

foo2 : Foo
foo2 = MkFoo Nat Int

test : Nat
test = baz foo2 foo1

{-
Type mismatch between
        (a = b) -> (to b = from a) -> from b -> to a (Type of baz a b)
and
        Nat (Expected type)
-}

baz : (a : Foo) -> (b : Foo) -> (prf : Foo.to b = Foo.from a) => (x : from b) => to a
baz a b =
  let y = bar b x
  in bar a (rewrite sym prf in y)

Working Version

record Foo where
  constructor MkFoo
  from : Type
  to : Type

bar : (a : Foo) -> (x : from a) -> (to a)
-- impl not important

baz : (a : Foo) -> (b : Foo) -> (from a = to b) -> (x : from b) -> to a
baz a b prf x =
  let y = bar b x
  in bar a (rewrite prf in y)

foo1 : Foo
foo1 = MkFoo String Nat

foo2 : Foo
foo2 = MkFoo Nat Int

test : Int
test = baz foo2 foo1 %implementation "test"

record Foo where
  constructor MkFoo
  from : Type
  to : Type

bar : (a : Foo) -> (x : from a) -> (to a)
-- impl not important

baz : (a : Foo) -> (b : Foo) -> (prf : Foo.to b = Foo.from a) => (x : from b) => to a
baz a b =
  let y = bar b x
  in bar a (rewrite sym prf in y)

foo1 : Foo
foo1 = MkFoo Nat String

foo2 : Foo
foo2 = MkFoo String Int

test : Int
test = baz foo2 foo1