@@ -1216,18 +1216,16 @@ object ElabHandler extends Handler[ElabConstraint]:
12161216 fillResultOnce(resultCell, accessAst)
12171217 module.readStable(solver, targetTy) match
12181218 case None =>
1219- lhs match
1220- case CST .Symbol (sym, _) =>
1221- (for
1222- id <- ctx.lookup(sym)
1223- tyCell <- ctx.lookupType(id)
1224- ty <- module.readStable(solver, tyCell)
1225- yield (id, ty)) match
1226- case Some ((id, AST .RecordTypeRef (recId, _, _))) =>
1227- ctx.lookupRecordById(recId).flatMap(_.fields.find(_.name == field)) match
1228- case Some (param) => fillResultOnce(inferredTyCell, param.ty)
1229- case None => fillResultOnce(inferredTyCell, AST .AnyType (span))
1230- case _ => ()
1219+ val CST .Symbol (sym, _) = lhs : @ unchecked
1220+ (for
1221+ id <- ctx.lookup(sym)
1222+ tyCell <- ctx.lookupType(id)
1223+ ty <- module.readStable(solver, tyCell)
1224+ yield (id, ty)) match
1225+ case Some ((_, AST .RecordTypeRef (recId, _, _))) =>
1226+ ctx.lookupRecordById(recId).flatMap(_.fields.find(_.name == field)) match
1227+ case Some (param) => fillResultOnce(inferredTyCell, param.ty)
1228+ case None => fillResultOnce(inferredTyCell, AST .AnyType (span))
12311229 case _ => ()
12321230 if ! module.hasSomeValue(solver, inferredTyCell.asInstanceOf [module.CellAny ]) then
12331231 fillResultOnce(inferredTyCell, AST .MetaCell (HoldNotReadable (targetTy), span))
@@ -3039,8 +3037,8 @@ object Elaborator:
30393037 module.run(solver)
30403038
30413039 val reports = reporter match
3042- case vr : VectorReporter [ElabProblem ] => vr.getReports
3043- case _ => Vector .empty
3040+ case vr : VectorReporter [? ] => vr.getReports. asInstanceOf [ Vector [ ElabProblem ]]
3041+ case _ => Vector .empty
30443042
30453043 results.map { (resCell, tyCell) =>
30463044 val astOpt = module.readStable(solver, resCell).map(r => substituteSolutions(r)(using module, solver))
0 commit comments