fails-on-an-input-that-is-not-a-normal-form.yaml

# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
# SPDX-License-Identifier: MIT
---
# 𝕄 maps normal forms to formations, and 'morph' does not normalize what it is
# handed. A dispatch off a formation with neither φ nor λ is not a normal form,
# since 'dot' of normalization eats it, so the run refuses it as broken input
# instead of failing with a bare "user error" (#1442, #2343).
location: 'Q.t'
input: '⟦ t ↦ ⟦ x ↦ ⟦⟧ ⟧.x ⟧'
fails: >-
  Morphing expects a normal form, but the term at the locator is not one:
  ⟦⟧:x.x