From 16e6325df30b3628717b0d2b91e0ad0b25d16be9 Mon Sep 17 00:00:00 2001
From: Steve Dunham <dunhamsteve@gmail.com>
Date: Mon, 28 Oct 2024 21:37:02 -0700
Subject: [PATCH] check for implicit

---
 src/Lib/Elab.idr | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/Lib/Elab.idr b/src/Lib/Elab.idr
index d964f9f..d281091 100644
--- a/src/Lib/Elab.idr
+++ b/src/Lib/Elab.idr
@@ -833,6 +833,8 @@ check ctx tm ty = case (tm, !(forceType ty)) of
     sc <- check (extend ctx nm' a) tm ty'
     pure $ Lam (getFC tm) nm' sc
 
+  (RImplicit fc, ty) => freshMeta ctx fc ty Normal
+
   (RLet fc nm ty v sc, rty) => do
     ty' <- check ctx ty (VU emptyFC)
     vty <- eval ctx.env CBN ty'