@@ -105,10 +105,23 @@ elabInstance info syn doc argDocs what fc cs acc opts n nfc ps t expn ds = do
105 let superclassInstances = map (substInstance ips pnames) (class_default_superclasses ci)
105 let superclassInstances = map (substInstance ips pnames) (class_default_superclasses ci)
106 undefinedSuperclassInstances <- filterM (fmap not . isOverlapping ist) superclassInstances
106 undefinedSuperclassInstances <- filterM (fmap not . isOverlapping ist) superclassInstances
107 mapM_ (rec_elabDecl info EAll info) undefinedSuperclassInstances
107 mapM_ (rec_elabDecl info EAll info) undefinedSuperclassInstances
110+ -- Bring variables in instance head into scope when building the
112+ let headVars = nub $ concatMap getHeadVars ps
113+ let (headVarTypes, ty)
114+ = case lookupTyExact iname (tt_ctxt ist) of
115+ Just ty -> (map (\n -> (n, getTypeIn ist n ty)) headVars, ty)
116+ _ -> (zip headVars (repeat Placeholder), Erased)
117+ logElab 3 $ "Head var types " ++ show headVarTypes ++ " from " ++ show ty
108 let all_meths = map (nsroot . fst) (class_methods ci)
119 let all_meths = map (nsroot . fst) (class_methods ci)
109 let mtys = map (\ (n, (op, t)) ->
120 let mtys = map (\ (n, (op, t)) ->
110 let t_in = substMatchesShadow ips pnames t
121 let t_in = substMatchesShadow ips pnames t
111− mnamemap = map (\n -> (n, PRef fc [] (decorate ns iname n)))
123+ map (\n -> (n, PApp fc (PRef fc [] (decorate ns iname n))
124+ (map (toImp fc) headVars)))
112 all_meths
125 all_meths
113 t' = substMatchesShadow mnamemap pnames t_in in
126 t' = substMatchesShadow mnamemap pnames t_in in
114 (decorate ns iname n,
127 (decorate ns iname n,
@@ -129,10 +142,7 @@ elabInstance info syn doc argDocs what fc cs acc opts n nfc ps t expn ds = do
129 logElab 3 $ "Instance is " ++ show ps ++ " implicits " ++
142 logElab 3 $ "Instance is " ++ show ps ++ " implicits " ++
130 show (concat (nub wparams))
143 show (concat (nub wparams))
132− -- Bring variables in instance head into scope when building the
145+
134− let headVars = nub $ concatMap getHeadVars ps
136 let lhsImps = map (\n -> pimp n (PRef fc [] n) True) headVars
146 let lhsImps = map (\n -> pimp n (PRef fc [] n) True) headVars
138 let lhs = PApp fc (PRef fc [] iname) lhsImps
148 let lhs = PApp fc (PRef fc [] iname) lhsImps
@@ -149,7 +159,7 @@ elabInstance info syn doc argDocs what fc cs acc opts n nfc ps t expn ds = do
149 let idecls = [PClauses fc totopts iname
159 let idecls = [PClauses fc totopts iname
150 [PClause fc iname lhs [] rhs []]]
160 [PClause fc iname lhs [] rhs []]]
152− mapM_ (rec_elabDecl info EAll info) (map (impBind headVars) wbTys)
162+ mapM_ (rec_elabDecl info EAll info) (map (impBind headVarTypes) wbTys)
153 mapM_ (rec_elabDecl info EAll info) idecls
163 mapM_ (rec_elabDecl info EAll info) idecls
155 ctxt <- getContext
165 ctxt <- getContext
@@ -246,9 +256,11 @@ elabInstance info syn doc argDocs what fc cs acc opts n nfc ps t expn ds = do
246 map snd (filter (\(i, _) -> i `elem` dets) a')
256 map snd (filter (\(i, _) -> i `elem` dets) a')
247 keepDets dets t = t
257 keepDets dets t = t
249− mkMethApp ps (n, _, _, ty)
259+ mkMethApp ps (n, _, _, ty)
250− = lamBind 0 ty (papp fc (PRef fc [] n)
260+ = lamBind 0 ty (papp fc (PRef fc [] n)
251− (ps ++ methArgs 0 ty))
261+ (ps ++ methArgs 0 ty))
263+ needed is p = pname p `elem` map pname is
252 lamBind i (PPi (Constraint _ _) _ _ _ sc) sc'
264 lamBind i (PPi (Constraint _ _) _ _ _ sc) sc'
253 = PLam fc (sMN i "meth") NoFC Placeholder (lamBind (i+1) sc sc')
265 = PLam fc (sMN i "meth") NoFC Placeholder (lamBind (i+1) sc sc')
254 lamBind i (PPi _ n _ ty sc) sc'
266 lamBind i (PPi _ n _ ty sc) sc'
@@ -346,19 +358,28 @@ getHeadVars (PDPair _ _ _ l t r) = getHeadVars l ++ getHeadVars t ++ getHeadVars
346getHeadVars _ = []
358getHeadVars _ = []
348-- Implicitly bind variables from the instance head in method types
360-- Implicitly bind variables from the instance head in method types
349−impBind :: [Name] -> PDecl -> PDecl
361+impBind :: [(Name, PTerm)] -> PDecl -> PDecl
350impBind vs (PTy d ds syn fc opts n fc' t)
362impBind vs (PTy d ds syn fc opts n fc' t)
351− = PTy d ds syn fc opts n fc' (doImpBind (vs \\ boundIn t) t)
363+ = PTy d ds syn fc opts n fc'
364+ (doImpBind (filter (\(n, ty) -> n `notElem` boundIn t) vs) t)
353 doImpBind [] ty = ty
366 doImpBind [] ty = ty
367+ doImpBind ((n, argty) : ns) ty
354− doImpBind (n : ns) ty = PPi impl n NoFC Placeholder (doImpBind ns ty)
368+ = PPi impl n NoFC argty (doImpBind ns ty)
356 boundIn (PPi _ n _ _ sc) = n : boundIn sc
370 boundIn (PPi _ n _ _ sc) = n : boundIn sc
357 boundIn _ = []
371 boundIn _ = []
373+getTypeIn :: IState -> Name -> Type -> PTerm
374+getTypeIn ist n (Bind x b sc)
375+ | n == x = delab ist (binderTy b)
376+ | otherwise = getTypeIn ist n (substV (P Ref x Erased) sc)
377+getTypeIn ist n tm = Placeholder
379+toImp fc n = pimp n (PRef fc [] n) True
360-- Propagate class parameters to method bodies, if they're not already
381-- Propagate class parameters to method bodies, if they're not already
361−-- there
382+-- there, and they are needed (i.e. appear in method's type)
362addParams :: [Name] -> PDecl -> PDecl
383addParams :: [Name] -> PDecl -> PDecl
363addParams ps (PClauses fc opts n cs) = PClauses fc opts n (map addCParams cs)
384addParams ps (PClauses fc opts n cs) = PClauses fc opts n (map addCParams cs)
@@ -369,13 +390,12 @@ addParams ps (PClauses fc opts n cs) = PClauses fc opts n (map addCParams cs)
369 (map (addParams ps) ds)
390 (map (addParams ps) ds)
370 addCParams c = c
391 addCParams c = c
393+ addTmParams ps (PRef fc hls n)
372− addTmParams ps (PRef fc hls n) = PApp fc (PRef fc hls n) (map toImp ps)
394+ = PApp fc (PRef fc hls n) (map (toImp fc) ps)
373 addTmParams ps (PApp fc ap@(PRef fc' hls n) args)
395 addTmParams ps (PApp fc ap@(PRef fc' hls n) args)
374− = PApp fc ap (mergePs (map toImp ps) args)
396+ = PApp fc ap (mergePs (map (toImp fc) ps) args)
375 addTmParams ps tm = tm
397 addTmParams ps tm = tm
377− toImp n = pimp n (PRef fc [] n) True
379 mergePs [] args = args
399 mergePs [] args = args
380 mergePs (p : ps) args
400 mergePs (p : ps) args
381 | isImplicit p,
401 | isImplicit p,