Bidirectional dependencies and Type Equality

Help
#1

Hello, I am confused by the type error when I am trying to compile this code:

import Type.Equality (class TypeEquals)

foo :: forall a. TypeEquals String a => a
foo = "hi"

“Could not match type String with type a0”

TypeEquals a b is a type class with a -> b, b -> a dependencies, which I thought the type checker should be able to realise a must be String.
Haskell gives the same error, but it has TypeFamilies so I can express this:

foo :: forall a. String ~ a => a

Is it a bug or is it intended?
Thank you very much!

#2

you have to use the to/from methods of the class to match them: https://pursuit.purescript.org/packages/purescript-type-equality/3.0.0/docs/Type.Equality#t:TypeEquals, since there’s no automatic behavior here

#3

How about if it’s not exactly TypeEquals?

class IntToString i s | i -> s, s -> i
instance i2s :: IntToString Int String

bar :: forall s. IntToString Int s => s
bar = "hi"
#4

This is expected behaviour; PureScript’s type checker doesn’t make use of type equalities like GHC’s can.

#5

Ok, thank you very much!