mirror of
https://github.com/idris-lang/Idris2.git
synced 2025-01-02 00:27:34 +03:00
45 lines
1.7 KiB
Plaintext
45 lines
1.7 KiB
Plaintext
1/1: Building Fld (Fld.idr)
|
|
Error: While processing type of myDog_shouldNotTypecheck0. Field not covered age.
|
|
|
|
Fld.idr:36:29--36:56
|
|
|
|
|
36 | myDog_shouldNotTypecheck0 : record MkDog {name = "Sam"} -- Not all fields are covered
|
|
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^
|
|
|
|
Error: While processing type of myDog_shouldNotTypecheck1. No constructor satisfies provided fields.
|
|
|
|
Fld.idr:38:29--38:66
|
|
|
|
|
38 | myDog_shouldNotTypecheck1 : record MkDog {age = 3, name1 = "Sam"} -- No constructor with name `MkDog`
|
|
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
|
|
|
|
Error: While processing type of myDog_shouldNotTypecheck2. Duplicate fields.
|
|
|
|
Fld.idr:40:29--44:47
|
|
40 | myDog_shouldNotTypecheck2 : record MkDog
|
|
41 | { age = 4
|
|
42 | , age = 2
|
|
43 | , weight = 12
|
|
44 | , name = "Sam" } -- Duplicate names
|
|
|
|
Error: While processing right hand side of r2_shouldNotTypecheck3. Ambiguous elaboration. Possible results:
|
|
Fld.R2.MkR ?field
|
|
Fld.R1.MkR ?field
|
|
|
|
Fld.idr:86:26--86:57
|
|
|
|
|
86 | r2_shouldNotTypecheck3 = record MkR {field = the Nat 22} -- fail, impossible to disambiguate
|
|
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
|
|
|
|
Error: While processing right hand side of r3_shouldNotTypecheck4. Can't infer type for this record.
|
|
|
|
Fld.idr:89:26--89:55
|
|
|
|
|
89 | r3_shouldNotTypecheck4 = record _ {field = the Nat 22} -- fail, impossible to disambiguate
|
|
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
|
|
|
|
Fld> Fld.myDog : OrdinaryDog
|
|
Fld> Fld.mySuperDog : SuperDog
|
|
Fld> Fld.other : Other String
|
|
Fld> Bye for now!
|