@@ -224,6 +224,8 @@ buildDepMap ci ctx mainName = addPostulates $ dfs S.empty M.empty [mainName]
225 -- get Deps for a Name
225 -- get Deps for a Name
226 getDeps :: Name -> Deps
226 getDeps :: Name -> Deps
227+ getDeps (SN (WhereN i (SN (InstanceCtorN classN)) (MN i' field)))
228+ = M.empty -- these deps are created when applying instance ctors
227 getDeps n = case lookupDef n ctx of
229 getDeps n = case lookupDef n ctx of
228 [def] -> getDepsDef n def
230 [def] -> getDepsDef n def
229 [] -> error $ "erasure checker: unknown reference: " ++ show n
231 [] -> error $ "erasure checker: unknown reference: " ++ show n
@@ -422,14 +424,25 @@ buildDepMap ci ctx mainName = addPostulates $ dfs S.empty M.empty [mainName]
422 getDepsTerm vs bs cd t = error $ "cannot get deps of: " ++ show t
424 getDepsTerm vs bs cd t = error $ "cannot get deps of: " ++ show t
424 -- Get the number of arguments that might be considered for erasure.
426 -- Get the number of arguments that might be considered for erasure.
425− -- If the symbol is unknown, we assume that it uses all its arguments.
426 getArity :: Name -> Int
427 getArity :: Name -> Int
429+ -- method, derive arity from the type of the instance ctor
430+ getArity (SN (WhereN i cn (MN i' field))) = case lookupDef cn ctx of
431+ [TyDecl (DCon tag arity) ty]
432+ -> let argTys = map snd $ getArgTys ty
433+ in if i < length argTys
434+ then length $ getArgTys (argTys !! i)
435+ else error $ "invalid method number " ++ show i ++ " for " ++ show cn
436+ _ -> error $ "could not find instance constructor " ++ show cn
427 getArity n = case lookupDef n ctx of
439 getArity n = case lookupDef n ctx of
428 [CaseOp ci ty tys def tot cdefs] -> length tys
440 [CaseOp ci ty tys def tot cdefs] -> length tys
429 [TyDecl (DCon tag arity) _] -> arity
441 [TyDecl (DCon tag arity) _] -> arity
430 [TyDecl (Ref) ty] -> length $ getArgTys ty
442 [TyDecl (Ref) ty] -> length $ getArgTys ty
431 [Operator ty arity op] -> arity
443 [Operator ty arity op] -> arity
444+ [] -> error $ "definition not found: " ++ show n
432− df -> error $ "unknown entity '" ++ show n ++ "' with definition: " ++ show df
445+ df -> error $ "unrecognised entity '" ++ show n ++ "' with definition: " ++ show df
434 -- convert applications of lambdas to lets
447 -- convert applications of lambdas to lets
435 -- Note that this transformation preserves de bruijn numbering
448 -- Note that this transformation preserves de bruijn numbering