Extracted from #2205 (comment)
module ConstraintPositionOddity where
import Data.HeytingAlgebra
data HeytingAlgebraDict a =
HeytingAlgebraDict
a -- ff
a -- tt
(a -> a -> a) -- implies
(a -> a -> a) -- conj
(a -> a -> a) -- disj
(a -> a) -- not
hafGood :: ∀ a b. HeytingAlgebra b => HeytingAlgebraDict (a -> b)
hafGood =
HeytingAlgebraDict
(\_ -> ff)
(\_ -> tt)
(\f g a -> f a `implies` g a)
(\f g a -> f a && g a)
(\f g a -> f a || g a)
(\f a -> not (f a))
hafBad :: ∀ a b. HeytingAlgebra b => HeytingAlgebraDict (a -> b)
hafBad =
HeytingAlgebraDict
_ff
_tt
_implies
_conj
_disj
_not
where
_ff _ = ff
_tt _ = tt
_implies f g a = f a `implies` g a
_conj f g a = f a && g a
_disj f g a = f a || g a
_not f a = not (f a)In the above, the hafGood typechecks just fine, hafBad fails with a "Could not match constrained type" error.
If you follow the link to comment at the top, it illustrates how the equation defs desguar differently than the lambdas, which results in the constraint being inferred like forall t1. t1 -> (forall a. (HeytingAlgebra a) => a) instead of forall t3 t4. (HeytingAlgebra t4) => t3 -> t4.
Extracted from #2205 (comment)
In the above, the
hafGoodtypechecks just fine,hafBadfails with a "Could not match constrained type" error.If you follow the link to comment at the top, it illustrates how the equation defs desguar differently than the lambdas, which results in the constraint being inferred like
forall t1. t1 -> (forall a. (HeytingAlgebra a) => a)instead offorall t3 t4. (HeytingAlgebra t4) => t3 -> t4.