Don’t look too much into what this code does, it’s just a small example of the behavior I was a little surprised at.
Two implementations of anyShow
, one using TypeEquals
and the other not. Sometimes they act the same, and sometimes they don’t. I’m guessing test4
works fine because it’s at the top level, whereas in test6
it is not, and the bidirectional type checker is doing something different for each as there’s different contexts?
module Main where
import Prelude
import Unsafe.Coerce
import Type.Proxy
import Type.Equality
anyShow1 :: forall a. Proxy a -> (Show a => String) -> String
anyShow1 _ f = (coerce f) { show: \_ -> "Shown" }
where
coerce :: (Show a => String) -> ({ show :: a -> String } -> String)
coerce = unsafeCoerce
anyShow2 :: forall a x. TypeEquals x (Show a => String) => Proxy a -> x -> String
anyShow2 _ f = (coerce f) { show: \_ -> "Shown" }
where
coerce :: x -> ({ show :: a -> String } -> String)
coerce = unsafeCoerce
data V = V
test1 = anyShow1 (Proxy :: _ V)
-- same type inferred for test2 as test1
test2 = anyShow2 (Proxy :: _ V)
test3 = test1 (show V)
test4 = test2 (show V)
test5 = anyShow1 (Proxy :: _ V) (show V)
-- doesn't work
-- Could not match constrained type `Show V => String` with type `String`
-- test6 = anyShow2 (Proxy :: _ V) (show V)
-- but does work with an explicit annotation
test7 = (anyShow2 (Proxy :: _ V) :: (Show V => String) -> String) (show V)