79423414

Date: 2025-02-08 15:17:28
Score: 0.5
Natty:
Report link

I reproduced the problem without ST monad. Now the problem is more visible. Function f5 cannot return type with s if s is marked as forall inside an implementation of the function.

data T1 s a = T1 a
data T2 s a = T2 a

f1 :: (forall s. T1 s a) -> a
f1 (T1 a) = a

f2 :: T1 s Integer
f2 = T1 1

f3 :: T1 s (T2 s Integer)
f3 = T1 (T2 1)

f4 :: Integer
f4 = f1 f2 -- OK, returns 1

f5 :: T2 s Integer
f5 = f1 f3 -- Error
--Couldn't match type `s1' with `s'
--Expected: T1 s1 (T2 s Integer)
--  Actual: T1 s1 (T2 s1 Integer)
Reasons:
  • Long answer (-0.5):
  • Has code block (-0.5):
  • Self-answer (0.5):
  • Low reputation (1):
Posted by: Dmitry Kapustin