So: what’s the point?

If you already have a b : Bool, you can turn it into proposition: So b, which is a bit shorther than b ≡ true. Sometimes (I don’t remember any actual case) there is no need to bother with a proper data type, and this quick solution is enough.

So seems to have serious disadvantages compared to a “proper”
proof-term: pattern matching on oh doesn’t give you any information
with which you could make another term type-check. As a corollary,
So values can’t usefully participate in interactive proving.
Contrast this with the computational usefulness of Disjoint, which
is represented as a list of proofs that each column in s' doesn’t
appear in s.

So does give you the same information as Disjoint — you just need to extract it. Basically, if there is no inconsistency between disjoint and Disjoint, then you should be able to write a function So (disjoint s) -> Disjoint s using pattern matching, recursion and impossible cases elimination.

However, if you tweak the definition a bit:

So : Bool -> Set
So true  = ⊤
So false = ⊥

So becomes a really useful data type, because x : So true immediately reduces to tt due to the eta-rule for ⊤. This allows to use So like a constraint: in pseudo-Haskell we could write

forall n. (n <=? 3) => Vec A n

and if n is in canonical form (i.e. suc (suc (suc ... zero))), then n <=? 3 can be checked by the compiler and no proofs are needed. In actual Agda it is

∀ {n} {_ : n <=? 3} -> Vec A n

I used this trick in this answer (it is {_ : False (m ≟ 0)} there). And I guess it would be impossible to write a usable version of the machinery decribed here without this simple definition:

Is-just : ∀ {α} {A : Set α} -> Maybe A -> Set
Is-just = T ∘ isJust

where T is So in the Agda’s standard library.

Also, in the presence of instance arguments So-as-a-data-type can be used as So-as-a-constraint:

open import Data.Bool.Base
open import Data.Nat.Base
open import Data.Vec

data So : Bool -> Set where
  oh : So true

instance
  oh-instance : So true
  oh-instance = oh

_<=_ : ℕ -> ℕ -> Bool
0     <= m     = true
suc n <= 0     = false
suc n <= suc m = n <= m

vec : ∀ {n} {{_ : So (n <= 3)}} -> Vec ℕ n
vec = replicate 0

ok : Vec ℕ 2
ok = vec

fail : Vec ℕ 4
fail = vec