------------------------------------------------------------------------
-- There is a term without a corresponding syntactic type (given some
-- assumptions)
------------------------------------------------------------------------

import Level
open import Universe

module README.DependentlyTyped.Term-without-type
  (Uni₀ : Universe Level.zero Level.zero)
  where

open import Data.Product
open import Function renaming (const to k)
import README.DependentlyTyped.NBE as NBE; open NBE Uni₀
import README.DependentlyTyped.NormalForm as NF; open NF Uni₀
import README.DependentlyTyped.Term as Term; open Term Uni₀
open import Relation.Binary.PropositionalEquality as P using (_≡_; _≢_)
open import Relation.Nullary

abstract

  -- There are no closed neutral terms.

  no-closed-neutral :  {σ}  ¬ (ε  σ  ne )
  no-closed-neutral (var ())
  no-closed-neutral (t₁ · t₂) = no-closed-neutral t₁

  -- There are no closed normal forms of "atomic" type.

  no-closed-atomic-normal :
     {σ}  ε  σ atomic-type  ¬ (ε  σ  no )
  no-closed-atomic-normal   (ne   t) = no-closed-neutral t
  no-closed-atomic-normal el (ne el t) = no-closed-neutral t

  -- There are no closed terms of "atomic" type (assuming
  -- extensionality).

  no-closed-atomic :
    P.Extensionality Level.zero Level.zero 
     {σ}  ε  σ atomic-type  ¬ (ε  σ)
  no-closed-atomic ext atomic t =
    no-closed-atomic-normal atomic (normalise ext t)

  -- There are terms without syntactic types, assuming that U₀ is
  -- inhabited (and also extensionality).
  --
  -- One could avoid this situation by annotating lambdas with the
  -- (syntactic) type of their domain. I tried this, and found it to
  -- be awkward. One case of the function
  -- README.DependentlyTyped.NBE.Value.řeify returns a lambda, and I
  -- didn't find a way to synthesise the annotation without supplying
  -- syntactic types to V̌alue, řeify, řeflect, etc.

  term-without-type :
    P.Extensionality Level.zero Level.zero  U₀ 
    ∃₂ λ Γ σ   λ (t : Γ  σ)  ¬ (Γ  σ type)
  term-without-type ext u = (ε , (, σ) , ƛ (var zero) , proof)
    where
    σ : IType ε (π el el)
    σ = k (U-π (U-el u) (k (U-el u)))

    proof :  {σ}  ¬ (ε  π el el , σ type)
    proof (π (el t) (el t′)) = no-closed-atomic ext  t