diff --git a/libs/base/Deriving/Common.idr b/libs/base/Deriving/Common.idr index b305fcf8f..c18834b85 100644 --- a/libs/base/Deriving/Common.idr +++ b/libs/base/Deriving/Common.idr @@ -48,16 +48,16 @@ wording Func = "a function name" wording (DataCon tag arity) = "a data constructor" wording (TyCon tag arity) = "a type constructor" -isTypeCon : Elaboration m => Name -> m (List (Name, TTImp)) -isTypeCon ty = do +isTypeCon : Elaboration m => FC -> Name -> m (List (Name, TTImp)) +isTypeCon fc ty = do [(_, MkNameInfo (TyCon _ _))] <- getInfo ty - | [] => fail "\{show ty} out of scope" - | [(_, MkNameInfo nt)] => fail "\{show ty} is \{wording nt} rather than a type constructor" - | _ => fail "\{show ty} is ambiguous" + | [] => failAt fc "\{show ty} out of scope" + | [(_, MkNameInfo nt)] => failAt fc "\{show ty} is \{wording nt} rather than a type constructor" + | _ => failAt fc "\{show ty} is ambiguous" cs <- getCons ty for cs $ \ n => do [(_, ty)] <- getType n - | _ => fail "\{show n} is ambiguous" + | _ => failAt fc "\{show n} is ambiguous" pure (n, ty) export @@ -65,7 +65,7 @@ isType : Elaboration m => TTImp -> m IsType isType = go Z [] where go : Nat -> List (Argument Name, Nat) -> TTImp -> m IsType - go idx acc (IVar _ n) = MkIsType n (map (map (minus idx . S)) acc) <$> isTypeCon n + go idx acc (IVar fc n) = MkIsType n (map (map (minus idx . S)) acc) <$> isTypeCon fc n go idx acc (IApp _ t (IVar _ nm)) = case nm of -- Unqualified: that's a local variable UN (Basic _) => go (S idx) ((Arg emptyFC nm, idx) :: acc) t @@ -78,7 +78,7 @@ isType = go Z [] where -- Unqualified: that's a local variable UN (Basic _) => go (S idx) ((AutoArg emptyFC nm, idx) :: acc) t _ => go (S idx) acc t - go idx acc t = fail "Expected a type constructor, got: \{show t}" + go idx acc t = failAt (getFC t) "Expected a type constructor, got: \{show t}" ------------------------------------------------------------------------------ -- Being a (data) constructor with a parameter diff --git a/tests/base/deriving_traversable/expected b/tests/base/deriving_traversable/expected index a1219727a..647d830cf 100644 --- a/tests/base/deriving_traversable/expected +++ b/tests/base/deriving_traversable/expected @@ -65,7 +65,7 @@ LOG derive.traversable.clauses:1: traverseIVect : {0 m : _} -> {0 a, b : Type} -> {0 f : Type -> Type} -> Applicative f => (a -> f b) -> IVect {n = m} a -> f (IVect {n = m} b) traverseIVect f (MkIVect x2) = MkIVect <$> (traverse f x2) LOG derive.traversable.clauses:1: - traverseEqMap : {0 key, eq : _} -> {0 a, b : Type} -> {0 f : Type -> Type} -> Applicative f => (a -> f b) -> EqMap key {{conArg:13919} = eq} a -> f (EqMap key {{conArg:13919} = eq} b) + traverseEqMap : {0 key, eq : _} -> {0 a, b : Type} -> {0 f : Type -> Type} -> Applicative f => (a -> f b) -> EqMap key {{conArg:13933} = eq} a -> f (EqMap key {{conArg:13933} = eq} b) traverseEqMap f (MkEqMap x3) = MkEqMap <$> (traverse (traverse f) x3) LOG derive.traversable.clauses:1: traverseTree : {0 l : _} -> {0 a, b : Type} -> {0 f : Type -> Type} -> Applicative f => (a -> f b) -> Tree l a -> f (Tree l b)