From c7fcb2c5a7c39b09a29cae22330b700e29baee21 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 18 Feb 2020 09:12:31 -0800 Subject: [PATCH] fix: missing `ensureHasType` --- src/Init/Lean/Elab/StructInst.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Init/Lean/Elab/StructInst.lean b/src/Init/Lean/Elab/StructInst.lean index c5851f8527..b806b74111 100644 --- a/src/Init/Lean/Elab/StructInst.lean +++ b/src/Init/Lean/Elab/StructInst.lean @@ -529,8 +529,8 @@ private partial def elabStruct : Struct → Option Expr → TermElabM (Expr × S pure (e, type, field::fields) }; match field.val with - | FieldVal.term stx => do val ← elabTerm stx (some d); continue val field - | FieldVal.nested s => do (val, sNew) ← elabStruct s (some d); continue val { val := FieldVal.nested sNew, .. field } + | FieldVal.term stx => do val ← elabTerm stx (some d); val ← ensureHasType stx d val; continue val field + | FieldVal.nested s => do (val, sNew) ← elabStruct s (some d); val ← ensureHasType s.ref d val; continue val { val := FieldVal.nested sNew, .. field } | FieldVal.default => do val ← mkFreshExprMVar field.ref (some d); continue (markDefaultMissing val) field | _ => throwFailedToElabField field.ref fieldName s.structName ("unexpected constructor type" ++ indentExpr type) | _ => throwError field.ref "unexpected unexpanded structure field")