mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-25 12:42:02 +03:00
2df3ecc2e3
We need to store the Context in errors at the point where the error occurs, or we might get some nonsense in the message. There's still a couple of places in Error where we don't do this right. This fixes one of them, and improves a few messages in the process.
169 lines
6.2 KiB
Plaintext
169 lines
6.2 KiB
Plaintext
1/1: Building Fld (Fld.idr)
|
|
Warning: We are about to implicitly bind the following lowercase names.
|
|
You may be unintentionally shadowing the associated global definitions:
|
|
a is shadowing Main.R1.R1.a
|
|
|
|
Fld:66:11--66:20
|
|
62 |
|
|
63 | public export
|
|
64 | record R2 where
|
|
65 | constructor MkR
|
|
66 | {auto field : a}
|
|
^^^^^^^^^
|
|
|
|
Warning: We are about to implicitly bind the following lowercase names.
|
|
You may be unintentionally shadowing the associated global definitions:
|
|
a is shadowing Main.R2.R2.a, Main.R1.R1.a
|
|
|
|
Fld:74:1--79:38
|
|
74 | interface Show a => (num : Num a) => MyIface a where -- Some interface with
|
|
75 | constructor MkIface
|
|
76 | -- constraints
|
|
77 | data MyData : a -> Type -- and a data declaration.
|
|
78 | someFunc : a -> a -- Constraints are now elaborated as auto implicits (as one would expect)
|
|
79 | giveBack : {x : a} -> MyData x -> a -- (previously as explicit arguments of the interface
|
|
|
|
Warning: We are about to implicitly bind the following lowercase names.
|
|
You may be unintentionally shadowing the associated global definitions:
|
|
a is shadowing Main.R2.R2.a, Main.R1.R1.a
|
|
|
|
Fld:74:1--79:38
|
|
74 | interface Show a => (num : Num a) => MyIface a where -- Some interface with
|
|
75 | constructor MkIface
|
|
76 | -- constraints
|
|
77 | data MyData : a -> Type -- and a data declaration.
|
|
78 | someFunc : a -> a -- Constraints are now elaborated as auto implicits (as one would expect)
|
|
79 | giveBack : {x : a} -> MyData x -> a -- (previously as explicit arguments of the interface
|
|
|
|
Warning: We are about to implicitly bind the following lowercase names.
|
|
You may be unintentionally shadowing the associated global definitions:
|
|
a is shadowing Main.R2.R2.a, Main.R1.R1.a
|
|
|
|
Fld:83:1--84:37
|
|
83 | data MyDataImpl : a -> Type where -- implementation of MyData
|
|
84 | MkMyData : (x : a) -> MyDataImpl x
|
|
|
|
Warning: We are about to implicitly bind the following lowercase names.
|
|
You may be unintentionally shadowing the associated global definitions:
|
|
a is shadowing Main.R2.R2.a, Main.R1.R1.a
|
|
|
|
Fld:84:3--84:11
|
|
80 | -- constructor)
|
|
81 |
|
|
82 |
|
|
83 | data MyDataImpl : a -> Type where -- implementation of MyData
|
|
84 | MkMyData : (x : a) -> MyDataImpl x
|
|
^^^^^^^^
|
|
|
|
Warning: We are about to implicitly bind the following lowercase names.
|
|
You may be unintentionally shadowing the associated global definitions:
|
|
a is shadowing Main.R2.R2.a, Main.R1.R1.a
|
|
|
|
Fld:110:1--110:11
|
|
106 | Show' String where
|
|
107 | show' = id
|
|
108 |
|
|
109 | %hint
|
|
110 | showMaybe' : Show' a => Show' (Maybe a)
|
|
^^^^^^^^^^
|
|
|
|
Warning: We are about to implicitly bind the following lowercase names.
|
|
You may be unintentionally shadowing the associated global definitions:
|
|
a is shadowing Main.R2.R2.a, Main.R1.R1.a
|
|
b is shadowing Main.Other.b
|
|
|
|
Fld:139:3--139:10
|
|
135 | setName : String -> OrdinaryDog -> OrdinaryDog
|
|
136 | setName name' = {name := name'}
|
|
137 |
|
|
138 | data Three : Type -> Type -> Type -> Type where
|
|
139 | MkThree : (x : a) -> (y : b) -> (z : c) -> Three a b c
|
|
^^^^^^^
|
|
|
|
Warning: We are about to implicitly bind the following lowercase names.
|
|
You may be unintentionally shadowing the associated global definitions:
|
|
a is shadowing Main.R2.R2.a, Main.R1.R1.a
|
|
b is shadowing Main.Other.b
|
|
|
|
Fld:141:1--141:10
|
|
137 |
|
|
138 | data Three : Type -> Type -> Type -> Type where
|
|
139 | MkThree : (x : a) -> (y : b) -> (z : c) -> Three a b c
|
|
140 |
|
|
141 | mapSetMap : (a -> a') -> b' -> (c -> c') -> Three a b c -> Three a' b' c'
|
|
^^^^^^^^^
|
|
|
|
Warning: We are about to implicitly bind the following lowercase names.
|
|
You may be unintentionally shadowing the associated global definitions:
|
|
a is shadowing Main.R2.R2.a, Main.R1.R1.a
|
|
|
|
Fld:217:15--217:21
|
|
213 | dontCare2 : (x : Nat) -> Nat -> Nat -> Nat -> (y : Nat) -> x + y = y + x
|
|
214 | dontCare2 {} = plusCommutative {}
|
|
215 | -- dontCare2 _ _ _ _ _ = plusCommutative _ _
|
|
216 |
|
|
217 | data Tree a = Leaf a | Node (Tree a) a (Tree a)
|
|
^^^^^^
|
|
|
|
Warning: We are about to implicitly bind the following lowercase names.
|
|
You may be unintentionally shadowing the associated global definitions:
|
|
a is shadowing Main.R2.R2.a, Main.R1.R1.a
|
|
|
|
Fld:217:24--217:48
|
|
213 | dontCare2 : (x : Nat) -> Nat -> Nat -> Nat -> (y : Nat) -> x + y = y + x
|
|
214 | dontCare2 {} = plusCommutative {}
|
|
215 | -- dontCare2 _ _ _ _ _ = plusCommutative _ _
|
|
216 |
|
|
217 | data Tree a = Leaf a | Node (Tree a) a (Tree a)
|
|
^^^^^^^^^^^^^^^^^^^^^^^^
|
|
|
|
Warning: We are about to implicitly bind the following lowercase names.
|
|
You may be unintentionally shadowing the associated global definitions:
|
|
a is shadowing Main.R2.R2.a, Main.R1.R1.a
|
|
|
|
Fld:219:1--219:7
|
|
215 | -- dontCare2 _ _ _ _ _ = plusCommutative _ _
|
|
216 |
|
|
217 | data Tree a = Leaf a | Node (Tree a) a (Tree a)
|
|
218 |
|
|
219 | isNode : Tree a -> Bool
|
|
^^^^^^
|
|
|
|
Warning: We are about to implicitly bind the following lowercase names.
|
|
You may be unintentionally shadowing the associated global definitions:
|
|
a is shadowing Main.R2.R2.a, Main.R1.R1.a
|
|
|
|
Fld:223:1--224:24
|
|
223 | data IsNode : Tree a -> Type where
|
|
224 | Is : IsNode (Node {})
|
|
|
|
Warning: We are about to implicitly bind the following lowercase names.
|
|
You may be unintentionally shadowing the associated global definitions:
|
|
a is shadowing Main.R2.R2.a, Main.R1.R1.a
|
|
|
|
Fld:226:1--226:10
|
|
222 |
|
|
223 | data IsNode : Tree a -> Type where
|
|
224 | Is : IsNode (Node {})
|
|
225 |
|
|
226 | decIsNode : (x : Tree a) -> Dec (IsNode x)
|
|
^^^^^^^^^
|
|
|
|
Error: While processing right hand side of r2_shouldNotTypecheck1. Ambiguous elaboration. Possible results:
|
|
Main.R2.MkR
|
|
Main.R1.MkR (Prelude.the Prelude.Nat 22)
|
|
|
|
Fld:72:26--72:29
|
|
68 | r1 : R1 -- explicit fields access
|
|
69 | r1 = MkR {field = "string"}
|
|
70 |
|
|
71 | r2_shouldNotTypecheck1 : ?
|
|
72 | r2_shouldNotTypecheck1 = MkR {field = the Nat 22} -- fail, impossible to disambiguate
|
|
^^^
|
|
|
|
Main> Main.myDog : OrdinaryDog
|
|
Main> Main.mySuperDog : SuperDog
|
|
Main> Main.other : Other String
|
|
Main> 1 hole: Main.r2_shouldNotTypecheck1 : ?_ [no locals in scope]
|
|
Main> Bye for now!
|