eliminating-merge.dhall

let -- The `Type` argument is needed so Dhall will let this be a `Kind`.
    Anc =
      < Abs | Rel : Type > : Kind

let -- `merge` works a the type level just fine
    Parents
    : Anc → Type
    = λ(anc : Anc) → merge { Abs = {}, Rel = λ(_ : Type) → Natural } anc

let -- `assert : {} ≡ Parents.Anc.Abs`, but Dhall doesn’t compare types
    works =
      Parents Anc.Abs

let -- `merge` can also go from a type to a term, just fine
    set
    : Anc → Natural → Optional Natural
    = λ(anc : Anc) →
      λ(n : Natural) →
        merge { Abs = None Natural, Rel = λ(_ : Type) → Some n } anc

let alsoWorks = assert : None Natural ≡ set Anc.Abs 1

let alsoWorks2 = assert : Some 2 ≡ set (Anc.Rel <>) 2

let -- `merge` can return terms of different types … sort of. If it sees them as
    --  the same “abstract” type. In this case, it always returns `Optional
    --  (Parents anc)`, nevermind that that will always resolve to `Optional {}`
    --  in the `None` case and `Optional Natural` in the `Some` case.
    setFrom =
      λ(anc : Anc) →
          ( λ(parents : Parents anc) →
              merge
                { Abs = None (Parents anc), Rel = λ(_ : Type) → Some parents }
                anc
          )
        : Parents anc → Optional (Parents anc)

let kindOfWorks
    : Optional {}
    = setFrom Anc.Abs {=}

let kindOfWorks2
    : Optional Natural
    = setFrom (Anc.Rel <>) 3

let -- but it doesn’t restrict the type within the scope of a `merge`. E.g.,
    -- here it can’t tell that `Some parents` will always have type `Optional
    -- Natural`, so it complains that the handlers have different output types,
    -- even though it must always be `Optional Natural`, and the previous case
    -- _doesn’t_ complain about different output types, even though it always
    -- returns different types in practice.
    doesntWork
    : Anc → Type → Optional Natural
    = λ(anc : Anc) →
      λ(parents : Parents anc) →
        merge { Abs = None Natural, Rel = λ(_ : Type) → Some parents } anc

let -- but no problem defining specialized versions, which is what I end up with
    insteadAbs =
      λ(parents : Parents Anc.Abs) → None Natural

let insteadRel = λ(parents : Parents (Anc.Rel <>)) → Some parents

in  Anc