@@ -224,6 +224,8 @@ buildDepMap ci ctx mainName = addPostulates $ dfs S.empty M.empty [mainName]
224224
225225 -- get Deps for a Name
226226 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
227229 getDeps n = case lookupDef n ctx of
228230 [def] -> getDepsDef n def
229231 [] -> error $ "erasure checker: unknown reference: " ++ show n
@@ -422,14 +424,25 @@ buildDepMap ci ctx mainName = addPostulates $ dfs S.empty M.empty [mainName]
422424 getDepsTerm vs bs cd t = error $ "cannot get deps of: " ++ show t
423425
424426 -- 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.
426427 getArity :: Name -> Int
428+
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
437+
438+ -- other names
427439 getArity n = case lookupDef n ctx of
428440 [CaseOp ci ty tys def tot cdefs] -> length tys
429441 [TyDecl (DCon tag arity) _] -> arity
430442 [TyDecl (Ref) ty] -> length $ getArgTys ty
431443 [Operator ty arity op] -> arity
432− df -> error $ "unknown entity '" ++ show n ++ "' with definition: " ++ show df
444+ [] -> error $ "definition not found: " ++ show n
445+ df -> error $ "unrecognised entity '" ++ show n ++ "' with definition: " ++ show df
433446
434447 -- convert applications of lambdas to lets
435448 -- Note that this transformation preserves de bruijn numbering