allow matching at 0 where appropriate

(for pairs, and for enums with 0 or 1 constructors)
This commit is contained in:
rhiannon morris 2023-03-27 00:08:09 +02:00
parent 137962c176
commit 7d36a7ff54

View file

@ -305,8 +305,9 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
} }
infer' ctx sg (CasePair pi pair ret body) = do infer' ctx sg (CasePair pi pair ret body) = do
-- if 1 ≤ π -- no check for 1 ≤ π, since pairs have a single constructor.
expectCompatQ one pi -- e.g. at 0 the components are also 0 in the body
--
-- if Ψ | Γ ⊢ σ · pair ⇒ (x : A) × B ⊳ Σ₁ -- if Ψ | Γ ⊢ σ · pair ⇒ (x : A) × B ⊳ Σ₁
pairres <- inferC ctx sg pair pairres <- inferC ctx sg pair
-- if Ψ | Γ, p : (x : A) × B ⊢₀ ret ⇐ Type -- if Ψ | Γ, p : (x : A) × B ⊢₀ ret ⇐ Type
@ -327,11 +328,11 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
} }
infer' ctx sg (CaseEnum pi t ret arms) {d, n} = do infer' ctx sg (CaseEnum pi t ret arms) {d, n} = do
-- if 1 ≤ π
expectCompatQ one pi
-- if Ψ | Γ ⊢ σ · t ⇒ {ts} ⊳ Σ₁ -- if Ψ | Γ ⊢ σ · t ⇒ {ts} ⊳ Σ₁
tres <- inferC ctx sg t tres <- inferC ctx sg t
ttags <- expectEnum !ask ctx tres.type ttags <- expectEnum !ask ctx tres.type
-- if 1 ≤ π, OR there is only zero or one option
unless (length (SortedSet.toList ttags) <= 1) $ expectCompatQ one pi
-- if Ψ | Γ, x : {ts} ⊢₀ A ⇐ Type -- if Ψ | Γ, x : {ts} ⊢₀ A ⇐ Type
checkTypeC (extendTy zero ret.name tres.type ctx) ret.term Nothing checkTypeC (extendTy zero ret.name tres.type ctx) ret.term Nothing
-- if for each "a ⇒ s" in arms, -- if for each "a ⇒ s" in arms,