I am having trouble understanding how type applications work. Why can sing in refuteRefuteKnockable be used without a type application when the call to sing in knockableOrOpened will fail to type check without a type application?
refuteRefuteKnockable :: SingI s => Refuted (Refuted (Knockable s)) -> Knockable s
refuteRefuteKnockable rrK =
case isKnockable $ sing of
Proved k -> k
Disproved rK -> absurd $ rrK rK
knockableOrOpened :: forall s. SingI s => Or Knockable ((:~:) Opened) s
knockableOrOpened =
case sing @s of
SOpened -> OrRight $ Refl
SClosed -> OrLeft KnockClosed
SLocked -> OrLeft KnockLocked
I am working from the following codebase: https://github.com/mstksg/inCode/blob/master/code-samples/singletons/Door3.hs
Type inference is the cause. This type contains s ...
refuteRefuteKnockable :: SingI s => Refuted (Refuted (Knockable s)) -> Knockable s
^^^^^^^^^^^
So, this
refuteRefuteKnockable rrK =
case isKnockable $ sing of
Proved k -> k
^^^
must have type Knockable s. Hence, the type of Proved k is inferred, probably containing s as well. That is the same type of isKnockable $ sing, from which we infer what type should be applied to sing (exploiting the signature of isKnockable). GHC does all of this for us.
In the latter example, we can't perform the same reasoning.
case sing of
SOpened -> OrRight $ Refl
SClosed -> OrLeft KnockClosed
SLocked -> OrLeft KnockLocked
is ambiguous because, even if the three branches must return a known type, we can still call sing on a different type then s and make everything typecheck. Since there isn't a unique s, inference can not work.
Note that above I had to guess a few things. If you shared the definitions of your types, we could be more accurate. (I.e., where is SOpened defined? What about Knockable, etc.?)
Collected from the Internet
Please contact [email protected] to delete if infringement.
Comments