Metavar solutions might contain 'let'

Mostly if they arise from search, where the target of the search has a
let in the type. So, we need to consider this when checking
metavariables in the linearity check.
This commit is contained in:
Edwin Brady 2020-03-19 22:14:57 +00:00
parent d666ed50c9
commit 7dcb1cfd34
2 changed files with 5 additions and 3 deletions

View File

@ -1068,8 +1068,8 @@ prettyName : {auto c : Ref Ctxt Defs} ->
Name -> Core String
prettyName (Nested i n)
= do i' <- toFullNames (Resolved i)
pure (show !(prettyName i') ++ "," ++
show !(prettyName n))
pure (!(prettyName i') ++ "," ++
!(prettyName n))
prettyName (CaseBlock outer idx)
= do outer' <- toFullNames (Resolved outer)
pure ("case block in " ++ !(prettyName outer'))

View File

@ -607,8 +607,10 @@ mutual
Core (Term vs)
substMeta (Bind bfc n (Lam c e ty) sc) (a :: as) env
= substMeta sc as (a :: env)
substMeta (Bind bfc n (Let c val ty) sc) as env
= substMeta (subst val sc) as env
substMeta rhs [] env = pure (substs env rhs)
substMeta rhs _ _ = throw (InternalError ("Badly formed metavar solution " ++ show n ++ " " ++ show rhs))
substMeta rhs _ _ = throw (InternalError ("Badly formed metavar solution " ++ show n ++ " " ++ show fn))
expandMeta rig erase env n idx def _
= throw (InternalError ("Badly formed metavar solution " ++ show n ++ " " ++ show def))