@@ -105,10 +105,23 @@ elabInstance info syn doc argDocs what fc cs acc opts n nfc ps t expn ds = do
105105 let superclassInstances = map (substInstance ips pnames) (class_default_superclasses ci)
106106 undefinedSuperclassInstances <- filterM (fmap not . isOverlapping ist) superclassInstances
107107 mapM_ (rec_elabDecl info EAll info) undefinedSuperclassInstances
108+
109+ ist <- getIState
110+ -- Bring variables in instance head into scope when building the
111+ -- dictionary
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
118+
108119 let all_meths = map (nsroot . fst) (class_methods ci)
109120 let mtys = map (\ (n, (op, t)) ->
110121 let t_in = substMatchesShadow ips pnames t
111− mnamemap = map (\n -> (n, PRef fc [] (decorate ns iname n)))
122+ mnamemap =
123+ map (\n -> (n, PApp fc (PRef fc [] (decorate ns iname n))
124+ (map (toImp fc) headVars)))
112125 all_meths
113126 t' = substMatchesShadow mnamemap pnames t_in in
114127 (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
129142 logElab 3 $ "Instance is " ++ show ps ++ " implicits " ++
130143 show (concat (nub wparams))
131144
132− -- Bring variables in instance head into scope when building the
133− -- dictionary
134− let headVars = nub $ concatMap getHeadVars ps
135−
145+
136146 let lhsImps = map (\n -> pimp n (PRef fc [] n) True) headVars
137147
138148 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
149159 let idecls = [PClauses fc totopts iname
150160 [PClause fc iname lhs [] rhs []]]
151161
152− mapM_ (rec_elabDecl info EAll info) (map (impBind headVars) wbTys)
162+ mapM_ (rec_elabDecl info EAll info) (map (impBind headVarTypes) wbTys)
153163 mapM_ (rec_elabDecl info EAll info) idecls
154164
155165 ctxt <- getContext
@@ -246,9 +256,11 @@ elabInstance info syn doc argDocs what fc cs acc opts n nfc ps t expn ds = do
246256 map snd (filter (\(i, _) -> i `elem` dets) a')
247257 keepDets dets t = t
248258
249− mkMethApp ps (n, _, _, ty)
250− = lamBind 0 ty (papp fc (PRef fc [] n)
251− (ps ++ methArgs 0 ty))
259+ mkMethApp ps (n, _, _, ty)
260+ = lamBind 0 ty (papp fc (PRef fc [] n)
261+ (ps ++ methArgs 0 ty))
262+ where
263+ needed is p = pname p `elem` map pname is
252264 lamBind i (PPi (Constraint _ _) _ _ _ sc) sc'
253265 = PLam fc (sMN i "meth") NoFC Placeholder (lamBind (i+1) sc sc')
254266 lamBind i (PPi _ n _ ty sc) sc'
@@ -346,19 +358,28 @@ getHeadVars (PDPair _ _ _ l t r) = getHeadVars l ++ getHeadVars t ++ getHeadVars
346358getHeadVars _ = []
347359
348360-- Implicitly bind variables from the instance head in method types
349−impBind :: [Name] -> PDecl -> PDecl
361+impBind :: [(Name, PTerm)] -> PDecl -> PDecl
350362impBind 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)
352365 where
353366 doImpBind [] ty = ty
354− doImpBind (n : ns) ty = PPi impl n NoFC Placeholder (doImpBind ns ty)
367+ doImpBind ((n, argty) : ns) ty
368+ = PPi impl n NoFC argty (doImpBind ns ty)
355369
356370 boundIn (PPi _ n _ _ sc) = n : boundIn sc
357371 boundIn _ = []
358372
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
378+
379+toImp fc n = pimp n (PRef fc [] n) True
359380
360381-- 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)
362383addParams :: [Name] -> PDecl -> PDecl
363384addParams ps (PClauses fc opts n cs) = PClauses fc opts n (map addCParams cs)
364385 where
@@ -369,13 +390,12 @@ addParams ps (PClauses fc opts n cs) = PClauses fc opts n (map addCParams cs)
369390 (map (addParams ps) ds)
370391 addCParams c = c
371392
372− addTmParams ps (PRef fc hls n) = PApp fc (PRef fc hls n) (map toImp ps)
393+ addTmParams ps (PRef fc hls n)
394+ = PApp fc (PRef fc hls n) (map (toImp fc) ps)
373395 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)
375397 addTmParams ps tm = tm
376398
377− toImp n = pimp n (PRef fc [] n) True
378−
379399 mergePs [] args = args
380400 mergePs (p : ps) args
381401 | isImplicit p,