JS
вот даже так
Could not deduce (Eq a) arising from a use of ‘==’
from the context: If flag (Eq a) (Eq a)KnownBool чтобы на рантайме различать True и False в типах, тогда в одной из веток такого ифа мы знаем что c ~ Int, соотв. Eq c, в другой мы просто знаем Eq c, соотв можем достать словарь.type Dict :: Constraint -> TypeНо теперь надо везде таскать этот
data Dict c = c => Dict
type Top :: Constraint
type Top = ()
type If :: Bool -> a -> a -> a
type family If i t e where
If 'True i _ = i
If 'False _ e = e
type KnownBool :: Bool -> Constraint
class KnownBool b where
sIf :: (b ~ 'True => r) -> (b ~ 'False => r) -> r
instance KnownBool 'True where sIf t _ = t
instance KnownBool 'False where sIf _ f = f
cmp :: forall flag a c . (If flag Top (Eq a), c ~ If flag Int a, KnownBool flag) => c -> c -> Bool
cmp a b | Dict :: Dict (Eq c) <- sIf @flag Dict Dict = a == b
KnownBool