Minimal reproduction for breaking Dhall's type system safety guarantees

soundness-violation.dhall

-- This is a minimal reproducing example of a major escape hatch that
-- violate's Dhall type safety guarantees.

let -- The uninhabited type (isomorphic to `< >`, but this is more ergonomic to
    -- use for this reproduction)
    Void : Type = ∀(any : Type) → any

let -- We model type-level negation in the standard way as a function from a
    -- given type to the uninhabited type.  `Not a` is only inhabited if `a`
    -- is uninhabited (i.e. isomorphic to `Void`)
    Not : Type → Type = λ(p : Type) → p → Void

let -- The powerset of `X`
    pow = λ(X : Kind) → X → Type

let -- If we define the following universe of over types:
    U = ∀(X : Kind) → (pow (pow X) → X) → pow (pow X)

let -- … and then introduce the following mapping:
    tau
        : pow (pow U) → U
        =   λ(t : pow (pow U))
          → λ(X : Kind)
          → λ(f : pow (pow X) → X)
          → λ(p : pow X)
          → t (λ(x : U) → p (f (x X f)))

in  -- The soundness issue is that nobody can force you to use Dhall for your
    -- project or, more generally, nobody can force you to use a language with
    -- language security worth a damn.  You can freely shoot yourself in the foot
    -- using Bash or YAML or whatever
    {=}