Why do some function calls fail to work without a type application?

Question

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

Answer 1

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.?)