Tips on dealing with errors?

cpitclaudel commented 3 years ago

Hi there,

In Kôika we have been deriving instances of custom EqDec and FiniteType typeclasses using Ltac, and the code is neither fast nor pretty, so I got intrigued by your Discourse announcement. Do you have tips on dealing with the following error? (I used the eqtype example from the readme on one of our types.

In environment
x : phantom Type reg_t
The term "x" has type "phantom Type reg_t" while it is expected to have type "phantom Type ?sT'".

The type that I'm looking at:

Inductive reg_t : Type :=
    toIMem : MemReq.reg_t -> reg_t
  | fromIMem : MemResp.reg_t -> reg_t
  | toDMem : MemReq.reg_t -> reg_t
  | fromDMem : MemResp.reg_t -> reg_t
  | f2d : fromFetch.reg_t -> reg_t
  | f2dprim : waitFromFetch.reg_t -> reg_t
  | d2e : fromDecode.reg_t -> reg_t
  | e2w : fromExecute.reg_t -> reg_t
  | rf : Rf.reg_t -> reg_t
  | mulState : Multiplier.reg_t -> reg_t
  | scoreboard : Scoreboard.reg_t -> reg_t
  | cycle_count : reg_t
  | instr_count : reg_t
  | pc : reg_t
  | epoch : reg_t

The first few constructors have parameters ….reg_t which are all relatively simple; for example:

Print MemReq.reg_t.
Inductive reg_t : Set :=  data0 : MemReq.reg_t | valid0 : MemReq.reg_t

Although the Rf.reg_t one is more complicated:

Print Rf.reg_t.
Inductive reg_t : Type :=  rData : index Rf.sz -> Rf.reg_t

(index is our fixpoint-based equivalent of Fin.t)

Let me know if you would like a pointer to the code.

cpitclaudel commented 3 years ago

I think it's likely that I'm doing something wrong though, because a simpler example fails too:

From mathcomp Require Import ssreflect ssrnat eqtype.
From deriving Require Import deriving.

Inductive reg_t := r0.

Definition reg_t_eqMixin := [derive eqMixin for reg_t].
Canonical reg_t_eqType := EqType reg_t reg_t_eqMixin.

cpitclaudel commented 3 years ago

(Btw, what's the foo_indMixin that the readme refers to? Should it be foo_indDef?)

arthuraa commented 3 years ago

(Btw, what's the foo_indMixin that the readme refers to? Should it be foo_indDef?)

It was a typo; thanks for catching it!

arthuraa commented 3 years ago

The error you saw arises because that notation triggers a canonical structure inference for an instance of indType over reg_t, which fails because no such instance has been declared. Here is the fix:

From mathcomp Require Import ssreflect ssrnat eqtype.
From deriving Require Import deriving.

Inductive reg_t := r0.
Definition reg_t_indDef := [indDef for reg_t_rect].
Canonical reg_t_indType := IndType reg_t reg_t_indDef.
Definition reg_t_eqMixin := [derive eqMixin for reg_t].
Canonical reg_t_eqType := EqType reg_t reg_t_eqMixin.

For your more complex type, before defining reg_t_eqMixin, you need to also make sure that every argument of reg_t is also declared as an instance of the class you are deriving (in this case, eqType). You don't need to declare instances of indType for them. Note that deriving does not provide support for types like index, so you would need to write an eqType instance for it by hand.

cpitclaudel commented 3 years ago

Thanks! I will look into all this :)

arthuraa / deriving

Tips on dealing with errors? #12