expected

TAbs_ Lam () (<[PVar_ () x]> TApp_ () (TPrim_ () (PrimBOp Gt)) (TTup_ () [TVar_ () 0@0,TNat_ () 3]))
TAbs_ Lam () (<[PAscr_ () (PVar_ () x) (TyAtom (ABase N))]> TApp_ () (TPrim_ () (PrimBOp Gt)) (TTup_ () [TVar_ () 0@0,TNat_ () 3]))
TAbs_ Lam () (<[PAscr_ () (PVar_ () x) (TyAtom (ABase N))]> TAbs_ Lam () (<[PVar_ () y]> TApp_ () (TPrim_ () (PrimBOp Gt)) (TTup_ () [TVar_ () 1@0,TVar_ () 0@0])))
TAbs_ Lam () (<[PAscr_ () (PVar_ () x) (TyAtom (ABase N))]> TAbs_ Lam () (<[PAscr_ () (PVar_ () y) (TyAtom (ABase F))]> TApp_ () (TPrim_ () (PrimBOp Gt)) (TTup_ () [TVar_ () 1@0,TVar_ () 0@0])))
TAbs_ Lam () (<[PVar_ () x]> TAbs_ Lam () (<[PAscr_ () (PVar_ () y) (TyAtom (ABase F))]> TApp_ () (TPrim_ () (PrimBOp Gt)) (TTup_ () [TVar_ () 1@0,TVar_ () 0@0])))
TAbs_ Lam () (<[PVar_ () x]> TApp_ () (TPrim_ () (PrimBOp Gt)) (TTup_ () [TVar_ () 0@0,TNat_ () 3]))
TAbs_ Lam () (<[PAscr_ () (PVar_ () x) (TyAtom (ABase N))]> TApp_ () (TPrim_ () (PrimBOp Gt)) (TTup_ () [TVar_ () 0@0,TNat_ () 3]))
TAbs_ Lam () (<[PAscr_ () (PVar_ () x) (TyAtom (ABase N))]> TAbs_ Lam () (<[PVar_ () y]> TApp_ () (TPrim_ () (PrimBOp Gt)) (TTup_ () [TVar_ () 1@0,TVar_ () 0@0])))
TAbs_ Lam () (<[PAscr_ () (PVar_ () x) (TyAtom (ABase N))]> TAbs_ Lam () (<[PAscr_ () (PVar_ () y) (TyAtom (ABase F))]> TApp_ () (TPrim_ () (PrimBOp Gt)) (TTup_ () [TVar_ () 1@0,TVar_ () 0@0])))
TAbs_ Lam () (<[PVar_ () x]> TAbs_ Lam () (<[PAscr_ () (PVar_ () y) (TyAtom (ABase F))]> TApp_ () (TPrim_ () (PrimBOp Gt)) (TTup_ () [TVar_ () 1@0,TVar_ () 0@0])))
8
Error: the shape of two types does not match.
https://disco-lang.readthedocs.io/en/latest/reference/shape-mismatch.html
8
8
1:16:
  |
1 | :parse exists x. x > 3
  |                ^
Variables introduced by ∀ or ∃ must have a type

TAbs_ Ex () (<[PAscr_ () (PVar_ () x) (TyAtom (ABase N))]> TApp_ () (TPrim_ () (PrimBOp Gt)) (TTup_ () [TVar_ () 0@0,TNat_ () 3]))
1:23:
  |
1 | :parse exists (x:N), y. x > y
  |                       ^
Variables introduced by ∀ or ∃ must have a type

TAbs_ Ex () (<[PAscr_ () (PVar_ () x) (TyAtom (ABase N)),PAscr_ () (PVar_ () y) (TyAtom (ABase F))]> TApp_ () (TPrim_ () (PrimBOp Gt)) (TTup_ () [TVar_ () 0@0,TVar_ () 0@1]))
1:16:
  |
1 | :parse exists x, (y:F). x > y
  |                ^
Variables introduced by ∀ or ∃ must have a type

1:11:
  |
1 | :parse ∃ x. x > 3
  |           ^
Variables introduced by ∀ or ∃ must have a type

TAbs_ Ex () (<[PAscr_ () (PVar_ () x) (TyAtom (ABase N))]> TApp_ () (TPrim_ () (PrimBOp Gt)) (TTup_ () [TVar_ () 0@0,TNat_ () 3]))
1:18:
  |
1 | :parse ∃ (x:N), y. x > y
  |                  ^
Variables introduced by ∀ or ∃ must have a type

TAbs_ Ex () (<[PAscr_ () (PVar_ () x) (TyAtom (ABase N)),PAscr_ () (PVar_ () y) (TyAtom (ABase F))]> TApp_ () (TPrim_ () (PrimBOp Gt)) (TTup_ () [TVar_ () 0@0,TVar_ () 0@1]))
1:11:
  |
1 | :parse ∃ x, (y:F). x > y
  |           ^
Variables introduced by ∀ or ∃ must have a type

1:16:
  |
1 | :parse forall x. x > 3
  |                ^
Variables introduced by ∀ or ∃ must have a type

TAbs_ All () (<[PAscr_ () (PVar_ () x) (TyAtom (ABase N))]> TApp_ () (TPrim_ () (PrimBOp Gt)) (TTup_ () [TVar_ () 0@0,TNat_ () 3]))
1:23:
  |
1 | :parse forall (x:N), y. x > y
  |                       ^
Variables introduced by ∀ or ∃ must have a type

TAbs_ All () (<[PAscr_ () (PVar_ () x) (TyAtom (ABase N)),PAscr_ () (PVar_ () y) (TyAtom (ABase F))]> TApp_ () (TPrim_ () (PrimBOp Gt)) (TTup_ () [TVar_ () 0@0,TVar_ () 0@1]))
1:16:
  |
1 | :parse forall x, (y:F). x > y
  |                ^
Variables introduced by ∀ or ∃ must have a type

1:11:
  |
1 | :parse ∀ x. x > 3
  |           ^
Variables introduced by ∀ or ∃ must have a type

TAbs_ All () (<[PAscr_ () (PVar_ () x) (TyAtom (ABase N))]> TApp_ () (TPrim_ () (PrimBOp Gt)) (TTup_ () [TVar_ () 0@0,TNat_ () 3]))
1:18:
  |
1 | :parse ∀ (x:N), y. x > y
  |                  ^
Variables introduced by ∀ or ∃ must have a type

TAbs_ All () (<[PAscr_ () (PVar_ () x) (TyAtom (ABase N)),PAscr_ () (PVar_ () y) (TyAtom (ABase F))]> TApp_ () (TPrim_ () (PrimBOp Gt)) (TTup_ () [TVar_ () 0@0,TVar_ () 0@1]))
1:11:
  |
1 | :parse ∀ x, (y:F). x > y
  |           ^
Variables introduced by ∀ or ∃ must have a type

TAbs_ All () (<[PTup_ () [PAscr_ () (PVar_ () x) (TyAtom (ABase N)),PAscr_ () (PVar_ () y) (TyAtom (ABase N)),PAscr_ () (PVar_ () z) (TyAtom (ABase N))]]> TApp_ () (TPrim_ () (PrimBOp Impl)) (TTup_ () [TApp_ () (TPrim_ () (PrimBOp And)) (TTup_ () [TParens_ () (TApp_ () (TPrim_ () (PrimBOp Eq)) (TTup_ () [TVar_ () 0@0,TVar_ () 0@1])),TParens_ () (TApp_ () (TPrim_ () (PrimBOp Eq)) (TTup_ () [TVar_ () 0@1,TVar_ () 0@2]))]),TApp_ () (TPrim_ () (PrimBOp Eq)) (TTup_ () [TVar_ () 0@0,TVar_ () 0@2])]))