0 | module TTImp.Elab.ImplicitBind

  4 | import Core.Coverage

  5 | import Core.Env

  6 | import Core.Metadata

  7 | import Core.Unify

  8 | import Core.Value

 10 | import Idris.REPL.Opts

 11 | import Idris.Syntax

 13 | import TTImp.Elab.Check

 14 | import TTImp.Elab.Delayed

 15 | import TTImp.TTImp

 17 | import Libraries.Data.NameMap

 18 | import Libraries.Data.SnocList.SizeOf

 20 | %default covering

 24 | mkOuterHole : {vars : _} ->

 25 |               {auto e : Ref EST (EState vars)} ->

 26 |               {auto c : Ref Ctxt Defs} ->

 27 |               {auto u : Ref UST UState} ->

 28 |               FC -> RigCount ->

 29 |               Name -> Env Term vars -> Maybe (Glued vars) ->

 30 |               Core (Term vars, Term vars)

 31 | mkOuterHole loc rig n topenv (Just expty_in)

 32 |     = do est <- get EST

 33 |          let sub = subEnv est

 34 |          expected <- getTerm expty_in

 35 |          case shrink expected sub of

 36 |               -- Can't shrink so rely on unification with expected type later

 37 |               Nothing => mkOuterHole loc rig n topenv Nothing

 38 |               Just exp' =>

 39 |                   do let env = outerEnv est

 40 |                      tm <- implBindVar loc rig env n exp'

 41 |                      pure (thin tm sub, thin exp' sub)

 42 | mkOuterHole loc rig n topenv Nothing

 43 |     = do est <- get EST

 44 |          let sub = subEnv est

 45 |          let env = outerEnv est

 46 |          nm <- genName ("type_of_" ++ nameRoot n)

 47 |          u <- uniVar loc

 48 |          ty <- metaVar loc erased env nm (TType loc u)

 49 |          log "elab.implicits" 10 $ "Made metavariable for type of " ++ show n ++ ": " ++ show nm

 50 |          put EST (addBindIfUnsolved nm loc rig Explicit topenv (thin ty sub) (TType loc u) est)

 51 |          tm <- implBindVar loc rig env n ty

 52 |          pure (thin tm sub, thin ty sub)

 60 | mkPatternHole : {vars' : _} ->

 61 |                 {auto e : Ref EST (EState vars')} ->

 62 |                 {auto c : Ref Ctxt Defs} ->

 63 |                 {auto u : Ref UST UState} ->

 64 |                 FC -> RigCount -> Name -> Env Term vars' -> BindMode ->

 65 |                 Maybe (Glued vars') ->

 66 |                 Core (Term vars', Term vars', Term vars')

 67 | mkPatternHole loc rig n env (PI _) exp

 68 |     = do (tm, exp) <- mkOuterHole loc rig n env exp

 69 |          pure (tm, exp, exp)

 70 | mkPatternHole {vars'} loc rig n topenv imode (Just expty_in)

 71 |     = do est <- get EST

 72 |          let sub = subEnv est

 73 |          let env = outerEnv est

 74 |          expected <- getTerm expty_in

 75 |          case bindInner topenv expected sub of

 76 |               Nothing => mkPatternHole loc rig n topenv imode Nothing

 77 |               Just exp' =>

 78 |                   do tm <- implBindVar loc rig env n exp'

 79 |                      pure (apply loc (thin tm sub) (mkArgs [<] sub),

 80 |                            expected,

 81 |                            thin exp' sub)

 82 |   where

 83 |     mkArgs : {0 vs : _} -> SizeOf seen -> Thin newvars vs -> List (Term (seen <>> vs))

 84 |     mkArgs p Refl = []

 85 |     mkArgs p (Drop th) =

 86 |       let MkVar v := mkVarChiply p in

 87 |       Local loc Nothing _ v :: mkArgs (p :< _) th

 88 |     mkArgs p _ = []

 90 |     -- This is for the specific situation where we're pattern matching on

 91 |     -- function types, which is realistically the only time we'll legitimately

 92 |     -- encounter a type variable under a binder

 93 |     bindInner : {vs : _} ->

 94 |                 Env Term vs -> Term vs -> Thin newvars vs ->

 95 |                 Maybe (Term newvars)

 96 |     bindInner env ty Refl = Just ty

 97 |     bindInner {vs = x :: _} (b :: env) ty (Drop p)

 98 |         = bindInner env (Bind loc x b ty) p

 99 |     bindInner _ _ _ = Nothing

101 | mkPatternHole loc rig n env _ _

102 |     = throw (GenericMsg loc ("Unknown type for pattern variable " ++ show n))

107 | normaliseType : {auto c : Ref Ctxt Defs} ->

108 |                 {free : _} ->

109 |                 Defs -> Env Term free -> Term free -> Core (Term free)

110 | normaliseType defs env tm

111 |     = catch (do tm' <- nfOpts withHoles defs env tm

112 |                 quoteOpts (MkQuoteOpts False False (Just 5)) defs env tm')

113 |             (\err => normalise defs env tm)

119 | bindUnsolved : {vars : _} ->

120 |                {auto c : Ref Ctxt Defs} ->

121 |                {auto e : Ref EST (EState vars)} ->

122 |                {auto u : Ref UST UState} ->

123 |                FC -> ElabMode -> BindMode -> Core ()

124 | bindUnsolved fc elabmode NONE = pure ()

125 | bindUnsolved {vars} fc elabmode _

126 |     = do est <- get EST

127 |          defs <- get Ctxt

128 |          let bifs = bindIfUnsolved est

129 |          log "elab.implicits" 5 $ "Bindable unsolved implicits: " ++ show (map fst bifs)

130 |          traverse_ (mkImplicit defs (outerEnv est) (subEnv est)) bifs

131 |   where

132 |     makeBoundVar : {outer, vs : _} ->

133 |                    Name -> FC -> RigCount -> PiInfo (Term vs) -> Env Term outer ->

134 |                    Thin outer vs -> Thin outer vars ->

135 |                    Term vs -> Core (Term vs)

136 |     makeBoundVar n loc rig p env sub subvars expected

137 |         = case shrink expected sub of

138 |                Nothing => do tmn <- toFullNames expected

139 |                              throw (GenericMsg fc ("Can't bind implicit " ++ show n ++ " of type " ++ show tmn))

140 |                Just exp' =>

141 |                     do impn <- genVarName (nameRoot n)

142 |                        tm <- metaVar fc rig env impn exp'

143 |                        let p' : PiInfo (Term vars) = forgetDef p

144 |                        update EST { toBind $= ((impn, NameBinding loc rig p'

145 |                                                         (thin tm subvars)

146 |                                                         (thin exp' subvars)) ::) }

147 |                        pure (thin tm sub)

149 |     mkImplicit : {outer : _} ->

150 |                  Defs -> Env Term outer -> Thin outer vars ->

151 |                  (Name, FC, RigCount, (vars' **

152 |                      (Env Term vars', PiInfo (Term vars'), Term vars', Term vars', Thin outer vars'))) ->

153 |                  Core ()

154 |     mkImplicit defs outerEnv subEnv (n, loc, rig, (vs ** (env, p, tm, exp, sub)))

155 |         = do Just (Hole {}) <- lookupDefExact n (gamma defs)

156 |                   | _ => pure ()

157 |              bindtm <- makeBoundVar n loc rig p outerEnv

158 |                                     sub subEnv

159 |                                     !(normaliseHoles defs env exp)

160 |              logTerm "elab.implicits" 5 ("Added unbound implicit") bindtm

161 |              ignore $ unify (case elabmode of

162 |                          InLHS _ => inLHS

163 |                          _ => inTerm)

164 |                    fc env tm bindtm

166 | swapIsVarH : {idx : Nat} -> (0 p : IsVar nm idx (x :: y :: xs)) ->

167 |              Var (y :: x :: xs)

168 | swapIsVarH First = MkVar (Later First)

169 | swapIsVarH (Later p) = swapP p -- it'd be nice to do this all at the top

170 |                                -- level, but that will need an improvement

171 |                                -- in erasability checking

172 |   where

173 |     swapP : forall name . {idx : _} -> (0 p : IsVar name idx (y :: xs)) ->

174 |             Var (y :: x :: xs)

175 |     swapP First = first

176 |     swapP (Later x) = MkVar (Later (Later x))

178 | swapIsVar : (vs : Scope) ->

179 |             {idx : Nat} -> (0 p : IsVar nm idx (vs ++ x :: y :: xs)) ->

180 |             Var (vs ++ y :: x :: xs)

181 | swapIsVar [] prf = swapIsVarH prf

182 | swapIsVar (x :: xs) First = first

183 | swapIsVar (x :: xs) (Later p)

184 |     = let MkVar p' = swapIsVar xs p in MkVar (Later p')

186 | swapVars : {vs : Scope} ->

187 |            Term (vs ++ x :: y :: ys) -> Term (vs ++ y :: x :: ys)

188 | swapVars (Local fc x idx p)

189 |     = let MkVar p' = swapIsVar _ p in Local fc x _ p'

190 | swapVars (Ref fc x name) = Ref fc x name

191 | swapVars (Meta fc n i xs) = Meta fc n i (map swapVars xs)

192 | swapVars {vs} (Bind fc x b scope)

193 |     = Bind fc x (map swapVars b) (swapVars {vs = x :: vs} scope)

194 | swapVars (App fc fn arg) = App fc (swapVars fn) (swapVars arg)

195 | swapVars (As fc s nm pat) = As fc s (swapVars nm) (swapVars pat)

196 | swapVars (TDelayed fc x tm) = TDelayed fc x (swapVars tm)

197 | swapVars (TDelay fc x ty tm) = TDelay fc x (swapVars ty) (swapVars tm)

198 | swapVars (TForce fc r tm) = TForce fc r (swapVars tm)

199 | swapVars (PrimVal fc c) = PrimVal fc c

200 | swapVars (Erased fc Impossible) = Erased fc Impossible

201 | swapVars (Erased fc Placeholder) = Erased fc Placeholder

202 | swapVars (Erased fc (Dotted t)) = Erased fc $ Dotted (swapVars t)

203 | swapVars (TType fc u) = TType fc u

208 | push : {vs : _} ->

209 |        FC -> (n : Name) -> Binder (Term vs) -> Term (n :: vs) -> Term vs

210 | push ofc n b tm@(Bind fc (PV x i) (Pi fc' c Implicit ty) sc) -- only push past 'PV's

211 |     = case shrink ty (Drop Refl) of

212 |            Nothing => -- needs explicit pi, do nothing

213 |                       Bind ofc n b tm

214 |            Just ty' => Bind fc (PV x i) (Pi fc' c Implicit ty')

215 |                             (push ofc n (map weaken b) (swapVars {vs = Scope.empty} sc))

216 | push ofc n b tm = Bind ofc n b tm

222 | liftImps : {vars : _} ->

223 |            BindMode -> (Term vars, Term vars) -> (Term vars, Term vars)

224 | liftImps (PI _) (tm, TType fc u) = (liftImps' tm, TType fc u)

225 |   where

226 |     liftImps' : {vars : _} ->

227 |                 Term vars -> Term vars

228 |     liftImps' (Bind fc (PV n i) b@(Pi _ _ Implicit _) sc)

229 |         = Bind fc (PV n i) b (liftImps' sc)

230 |     liftImps' (Bind fc n b@(Pi {}) sc)

231 |         = push fc n b (liftImps' sc)

232 |     liftImps' tm = tm

233 | liftImps _ x = x

236 | bindImplVars : FC -> BindMode ->

237 |                Defs ->

238 |                Env Term vars ->

239 |                List (Name, ImplBinding vars) ->

240 |                Term vars -> Term vars -> (Term vars, Term vars)

241 | bindImplVars fc NONE gam env imps_in scope scty = (scope, scty)

242 | bindImplVars {vars} fc mode gam env imps_in scope scty

243 |     = let imps = map (\ (x, bind) => (tidyName x, x, bind)) imps_in in

244 |           getBinds imps None scope scty

245 |   where

246 |     -- Turn the pattern variable name into the user's original choice,

247 |     -- now that there's no longer a risk of clash

248 |     tidyName : Name -> Name

249 |     tidyName (NS _ n) = tidyName n

250 |     tidyName (PV n _) = tidyName n

251 |     tidyName (Nested n inner) = tidyName inner

252 |     tidyName n = n

254 |     getBinds : (imps : List (Name, Name, ImplBinding vs)) ->

255 |                Bounds new -> (tm : Term vs) -> (ty : Term vs) ->

256 |                (Term (new ++ vs), Term (new ++ vs))

257 |     getBinds [] bs tm ty = (refsToLocals bs tm, refsToLocals bs ty)

258 |     getBinds {new} ((n, metan, NameBinding loc c p _ bty) :: imps) bs tm ty

259 |         = let (tm', ty') = getBinds imps (Add n metan bs) tm ty

260 |               bty' = refsToLocals bs bty in

261 |               case mode of

262 |                    PI c =>

263 |                       (Bind fc _ (Pi fc c Implicit bty') tm',

264 |                        TType fc (MN "top" 0))

265 |                    _ =>

266 |                       (Bind fc _ (PVar loc c (map (weakenNs (sizeOf bs)) p) bty') tm',

267 |                        Bind fc _ (PVTy fc c bty') ty')

268 |     getBinds ((n, metan, AsBinding c _ _ bty bpat) :: imps) bs tm ty

269 |         = let (tm', ty') = getBinds imps (Add n metan bs) tm ty

270 |               bty' = refsToLocals bs bty

271 |               bpat' = refsToLocals bs bpat in

272 |               (Bind fc _ (PLet fc c bpat' bty') tm',

273 |                Bind fc _ (PLet fc c bpat' bty') ty')

275 | normaliseHolesScope : {auto c : Ref Ctxt Defs} ->

276 |                       {vars : _} ->

277 |                       Defs -> Env Term vars -> Term vars -> Core (Term vars)

278 | normaliseHolesScope defs env (Bind fc n b sc)

279 |     = pure $ Bind fc n b

280 |                   !(normaliseHolesScope defs

281 |                    -- use Lam because we don't want it reducing in the scope

282 |                    (Lam fc (multiplicity b) Explicit (binderType b) :: env) sc)

283 | normaliseHolesScope defs env tm = normaliseHoles defs env tm

286 | bindImplicits : {vars : _} ->

287 |                 FC -> BindMode ->

288 |                 Defs -> Env Term vars ->

289 |                 List (Name, ImplBinding vars) ->

290 |                 Term vars -> Term vars -> Core (Term vars, Term vars)

291 | bindImplicits fc NONE defs env hs tm ty = pure (tm, ty)

292 | bindImplicits {vars} fc mode defs env hs tm ty

293 |    = pure $ liftImps mode $ bindImplVars fc mode defs env hs tm ty

296 | implicitBind : {auto c : Ref Ctxt Defs} ->

297 |                {auto u : Ref UST UState} ->

298 |                Name -> Core ()

299 | implicitBind n

300 |     = do defs <- get Ctxt

301 |          Just (Hole {}) <- lookupDefExact n (gamma defs)

302 |              | _ => pure ()

303 |          updateDef n (const (Just ImpBind))

304 |          removeHoleName n

312 | getToBind : {vars : _} ->

313 |             {auto c : Ref Ctxt Defs} ->

314 |             {auto e : Ref EST (EState vars)} ->

315 |             {auto u : Ref UST UState} ->

316 |             FC -> ElabMode -> BindMode ->

317 |             Env Term vars -> (excepts : List Name) ->

318 |             Core (List (Name, ImplBinding vars))

319 | getToBind fc elabmode NONE env excepts

320 |     = pure [] -- We should probably never get here, but for completeness...

321 | getToBind {vars} fc elabmode impmode env excepts

322 |     = do solveConstraints (case elabmode of

323 |                                 InLHS _ => inLHS

324 |                                 _ => inTerm) Normal

325 |          bindUnsolved fc elabmode impmode

326 |          solveConstraints (case elabmode of

327 |                                 InLHS _ => inLHS

328 |                                 _ => inTerm) Normal

329 |          defs <- get Ctxt

330 |          est <- get EST

331 |          let tob = reverse $ filter (\x => not (fst x `elem` excepts)) $

332 |                              toBind est

333 |          -- Make sure all the hole names are normalised in the implicitly

334 |          -- bound types, because otherwise we'll bind them too

335 |          res <- normImps defs [] tob

336 |          let hnames = map fst res

337 |          -- Return then in dependency order

338 |          let res' = depSort hnames res

339 |          log "elab.implicits" 10 $ "Bound names: " ++ show res

340 |          log "elab.implicits" 10 $ "Sorted: " ++ show res'

341 |          pure res'

342 |   where

343 |     normBindingTy : Defs -> ImplBinding vars -> Core (ImplBinding vars)

344 |     normBindingTy defs (NameBinding loc c p tm ty)

345 |         = do case impmode of

346 |                   COVERAGE => do tynf <- nf defs env ty

347 |                                  when !(isEmpty defs env tynf) $

348 |                                     throw ImpossibleCase

349 |                   _ => pure ()

350 |              pure $ NameBinding loc c p tm !(normaliseType defs env ty)

351 |     normBindingTy defs (AsBinding c p tm ty pat)

352 |         = do case impmode of

353 |                   COVERAGE => do tynf <- nf defs env ty

354 |                                  when !(isEmpty defs env tynf) $

355 |                                     throw ImpossibleCase

356 |                   _ => pure ()

357 |              pure $ AsBinding c p tm !(normaliseType defs env ty)

358 |                                      !(normaliseHoles defs env pat)

360 |     normImps : Defs -> List Name -> List (Name, ImplBinding vars) ->

361 |                Core (List (Name, ImplBinding vars))

362 |     normImps defs ns [] = pure []

363 |     normImps defs ns ((PV n i, bty) :: ts)

364 |         = do logTermNF "elab.implicits" 10 ("Implicit pattern var " ++ show (PV n i)) env

365 |                        (bindingType bty)

366 |              if PV n i `elem` ns

367 |                 then normImps defs ns ts

368 |                 else do rest <- normImps defs (PV n i :: ns) ts

369 |                         pure ((PV n i, !(normBindingTy defs bty)) :: rest)

370 |     normImps defs ns ((n, bty) :: ts)

371 |         = do tmnf <- normaliseHoles defs env (bindingTerm bty)

372 |              logTerm "elab.implicits" 10 ("Normalising implicit " ++ show n) tmnf

373 |              case getFnArgs tmnf of

374 |                 -- n reduces to another hole, n', so treat it as that as long

375 |                 -- as it isn't already done

376 |                 (Meta _ n' i margs, args) =>

377 |                     do hole <- isCurrentHole i

378 |                        if hole && not (n' `elem` ns)

379 |                           then do rest <- normImps defs (n' :: ns) ts

380 |                                   btynf <- normBindingTy defs bty

381 |                                   pure ((n', btynf) :: rest)

382 |                           else normImps defs ns ts

383 |                 _ => -- Unified to something concrete, so drop it

384 |                      normImps defs ns ts

386 |     -- Insert the hole/binding pair into the list before the first thing

387 |     -- which refers to it

388 |     insert : (Name, ImplBinding vars) -> List Name -> List Name ->

389 |              List (Name, ImplBinding vars) ->

390 |              List (Name, ImplBinding vars)

391 |     insert h ns sofar [] = [h]

392 |     insert (hn, bty) ns sofar ((hn', bty') :: rest)

393 |         = let used = filter (\n => elem n ns) (keys (bindingMetas bty')) in

394 |               -- 'used' is to make sure we're only worrying about metavariables

395 |               -- introduced in *this* expression (there may be others unresolved

396 |               -- from elsewhere, for type inference purposes)

397 |               if hn `elem` used

398 |                  then (hn, bty) ::

399 |                       (hn', bty') :: rest

400 |                  else (hn', bty') ::

401 |                           insert (hn, bty) ns (hn' :: sofar) rest

403 |     -- Sort the list of implicits so that each binding is inserted *after*

404 |     -- all the things it depends on (assumes no cycles)

405 |     depSort : List Name -> List (Name, ImplBinding vars) ->

406 |               List (Name, ImplBinding vars)

407 |     depSort hnames [] = []

408 |     depSort hnames (h :: hs) = insert h hnames [] (depSort hnames hs)

411 | checkBindVar : {vars : _} ->

412 |                {auto c : Ref Ctxt Defs} ->

413 |                {auto m : Ref MD Metadata} ->

414 |                {auto u : Ref UST UState} ->

415 |                {auto e : Ref EST (EState vars)} ->

416 |                {auto s : Ref Syn SyntaxInfo} ->

417 |                {auto o : Ref ROpts REPLOpts} ->

418 |                RigCount -> ElabInfo ->

419 |                NestedNames vars -> Env Term vars ->

420 |                FC -> Name ->

421 |                Maybe (Glued vars) ->

422 |                Core (Term vars, Glued vars)

423 | checkBindVar rig elabinfo nest env fc nm topexp

424 |     = do let elabmode = elabMode elabinfo

425 |          -- In types, don't rebind if the name is already in scope;

426 |          -- Below, return True if we don't need to implicitly bind the name

427 |          let False = case implicitMode elabinfo of

428 |                           PI _ => maybe False (const True) (defined nm env)

429 |                           _ => False

430 |                | _ => check rig elabinfo nest env (IVar fc nm) topexp

431 |          est <- get EST

432 |          let n = PV nm (defining est)

433 |          noteLHSPatVar elabmode nm

434 |          notePatVar n

435 |          est <- get EST

437 |          whenJust (isConcreteFC fc) $ \nfc => do

438 |            log "ide-mode.highlight" 7 $ "getNameType is adding Bound: " ++ show n

439 |            addSemanticDecorations [(nfc, Bound, Just n)]

442 |          case lookup n (boundNames est) of

443 |               Nothing =>

444 |                 do (tm, exp, bty) <- mkPatternHole fc rig n env

445 |                                               (implicitMode elabinfo)

446 |                                               topexp

447 |                    -- In PI mode, it's invertible like any other pi bound thing

448 |                    case implicitMode elabinfo of

449 |                         PI _ => setInvertible fc n

450 |                         _ => pure ()

451 |                    log "elab.implicits" 5 $ "Added Bound implicit " ++ show (n, (rig, tm, exp, bty))

452 |                    update EST { boundNames $= ((n, NameBinding fc rig Explicit tm exp) ::),

453 |                                 toBind $= ((n, NameBinding fc rig Explicit tm bty) :: ) }

455 |                    log "metadata.names" 7 $ "checkBindVar is adding ↓"

456 |                    addNameType fc nm env exp

457 |                    addNameLoc fc nm

459 |                    checkExp rig elabinfo env fc tm (gnf env exp) topexp

460 |               Just bty =>

461 |                 do -- Check rig is consistent with the one in bty, and

462 |                    -- update if necessary

463 |                    combine nm rig (bindingRig bty)

464 |                    let tm = bindingTerm bty

465 |                    let ty = bindingType bty

467 |                    log "metadata.names" 7 $ "checkBindVar is adding ↓"

468 |                    addNameType fc nm env ty

469 |                    addNameLoc fc nm

471 |                    checkExp rig elabinfo env fc tm (gnf env ty) topexp

472 |   where

473 |     updateRig : Name -> RigCount -> List (Name, ImplBinding vars) ->

474 |                 List (Name, ImplBinding vars)

475 |     updateRig n c [] = []

476 |     updateRig n c ((bn, r) :: bs)

477 |         = if n == bn

478 |              then case r of

479 |                   NameBinding loc _ p tm ty => (bn, NameBinding loc c p tm ty) :: bs

480 |                   AsBinding _ p tm ty pat => (bn, AsBinding c p tm ty pat) :: bs

481 |              else (bn, r) :: updateRig n c bs

483 |     -- Two variables are incompatble if at least one of them appears in a linear position

484 |     -- and their sum is bigger than 1

485 |     isIncompatible : RigCount -> RigCount -> Bool

486 |     isIncompatible l r = (isLinear l || isLinear r) && linear < l |+| r

488 |     combine : Name -> RigCount -> RigCount -> Core ()

489 |     combine n l r = when (isIncompatible l r)

490 |                          (throw (LinearUsed fc 2 n))

492 | checkPolyConstraint :

493 |             {auto c : Ref Ctxt Defs} ->

494 |             PolyConstraint -> Core ()

495 | checkPolyConstraint (MkPolyConstraint fc env arg x y)

496 |     = do defs <- get Ctxt

497 |          -- If 'x' is a metavariable and 'y' is concrete, that means we've

498 |          -- ended up putting something too concrete in for a polymorphic

499 |          -- argument

500 |          xnf <- continueNF defs env x

501 |          case xnf of

502 |               NApp _ (NMeta {}) _ =>

503 |                    do ynf <- continueNF defs env y

504 |                       if !(concrete defs env ynf)

505 |                          then do empty <- clearDefs defs

506 |                                  throw (MatchTooSpecific fc env arg)

507 |                          else pure ()

508 |               _ => pure ()

510 | solvePolyConstraint :

511 |             {auto c : Ref Ctxt Defs} ->

512 |             {auto u : Ref UST UState} ->

513 |             PolyConstraint -> Core ()

514 | solvePolyConstraint (MkPolyConstraint fc env arg x y)

515 |     = do defs <- get Ctxt

516 |          -- If the LHS of the constraint isn't a metavariable, we can solve

517 |          -- the constraint

518 |          case !(continueNF defs env x) of

519 |               xnf@(NApp _ (NMeta {}) _) => pure ()

520 |               t => do res <- unify inLHS fc env t !(continueNF defs env y)

521 |                       -- If there's any constraints, it just means we didn't

522 |                       -- solve anything and it won't help the check

523 |                       pure ()

526 | checkBindHere : {vars : _} ->

527 |                 {auto c : Ref Ctxt Defs} ->

528 |                 {auto m : Ref MD Metadata} ->

529 |                 {auto u : Ref UST UState} ->

530 |                 {auto e : Ref EST (EState vars)} ->

531 |                 {auto s : Ref Syn SyntaxInfo} ->

532 |                 {auto o : Ref ROpts REPLOpts} ->

533 |                 RigCount -> ElabInfo ->

534 |                 NestedNames vars -> Env Term vars ->

535 |                 FC -> BindMode -> RawImp ->

536 |                 Maybe (Glued vars) ->

537 |                 Core (Term vars, Glued vars)

538 | checkBindHere rig elabinfo nest env fc bindmode tm exp

539 |     = do est <- get EST

540 |          let oldenv = outerEnv est

541 |          let oldsub = subEnv est

542 |          let oldbif = bindIfUnsolved est

543 |          let dontbind = map fst (toBind est)

544 |          -- Set the binding environment in the elab state - unbound

545 |          -- implicits should have access to whatever is in scope here

546 |          put EST (updateEnv env Refl [] est)

547 |          constart <- getNextEntry

548 |          (tmv, tmt) <- check rig ({ implicitMode := bindmode,

549 |                                     bindingVars := True }

550 |                                   elabinfo)

551 |                              nest env tm exp

552 |          let solvemode = case elabMode elabinfo of

553 |                               InLHS c => inLHS

554 |                               _ => inTerm

555 |          solveConstraints solvemode Normal

557 |          ust <- get UST

558 |          catch (retryDelayed solvemode (delayedElab ust))

559 |                (\err =>

560 |                   do update UST { delayedElab := [] }

561 |                      throw err)

563 |          -- Check all the patterns standing for polymorphic variables are

564 |          -- indeed polymorphic

565 |          ust <- get UST

566 |          let cons = polyConstraints ust

567 |          put UST ({ polyConstraints := [] } ust)

568 |          traverse_ solvePolyConstraint cons

569 |          traverse_ checkPolyConstraint cons

571 |          solveConstraintsAfter constart

572 |                           (case elabMode elabinfo of

573 |                                 InLHS c => inLHS

574 |                                 _ => inTerm) Defaults

575 |          checkDots -- Check dot patterns unifying with the claimed thing

576 |                    -- before binding names

578 |          logTerm "elab.implicits" 5 "Binding names" tmv

579 |          logTermNF "elab.implicits" 5 "Normalised" env tmv

580 |          argImps <- getToBind fc (elabMode elabinfo)

581 |                               bindmode env dontbind

582 |          clearToBind dontbind

583 |          update EST $ updateEnv oldenv oldsub oldbif . { boundNames := [] }

584 |          ty <- getTerm tmt

585 |          defs <- get Ctxt

586 |          (bv, bt) <- bindImplicits fc bindmode

587 |                                    defs env argImps

588 |                                    !(normaliseHoles defs env tmv)

589 |                                    !(normaliseHoles defs env ty)

590 |          traverse_ implicitBind (map fst argImps)

591 |          checkExp rig elabinfo env fc bv (gnf env bt) exp