Consider the following code
data Foo f where
Foo :: Foo Int
class DynFoo t where
dynFoo :: Foo f -> Foo t
instance DynFoo Int where
dynFoo Foo = Foo
obsFoo :: (DynFoo t) => Foo f -> Foo t
obsFoo = dynFoo
useDynFoo :: Foo f -> Int
useDynFoo (obsFoo -> Foo) = 1
The pattern match in useDynFoo
should constrain the use of obsFoo
to have type Foo f -> Foo Int
, which should cause it to search for an instance of DynFoo Int
. However, it instead searches for an instance of DynFoo t
for unknown t
, and naturally fails.
No instance for (DynFoo t0) arising from a use of ‘obsFoo’
The type variable ‘t0’ is ambiguous
However, if I change the definition of useDynFoo
to
useDynFoo :: Foo f -> Int
useDynFoo (obsFoo -> (Foo :: Foo Int)) = 1
Then it suddenly works, even though my type signature is completely redundant.
So, why is this happening, and how can I use obsFoo
without having to give a type signature?