Gergely Buday (Mar 13 2024 at 15:35): Gergely Buday (Mar 13 2024 at 15:35):What the real problem can be when I get a type error that seems not to be an error?
Type error in application: incompatible operand type
Operator: (∘) (tlr fa) :: ('a ⇒ 'a × 'log) ⇒ 'a ⇒ 'b × 'log
Operand: rtf :: 'a ⇒ 'a × 'log
The argument of the operator has the very same type as the operand. I really wonder about this.
Manuel Eberl (Mar 13 2024 at 15:49):Maybe do a declare [[show_sorts]] before and check the sort constraints.
Manuel Eberl (Mar 13 2024 at 15:50):Or you can do declare [[unify_trace_failure]] and try to read the trace of that. Although I'd recommend only doing that right before the error occurs; otherwise there is too much of an overhead.
Manuel Eberl (Mar 13 2024 at 15:51):You can also do note [[unify_trace]] in an Isar proof or using [[unify_trace]] in a proof state.
Gergely Buday (Mar 13 2024 at 15:51):Manuel Eberl said:
Maybe do a
declare [[show_sorts]]before and check the sort constraints.
Yes that showed the problem and then I prescribed the type class constraint at some definitions and this cured the problem. Thanks.
Gergely Buday (Mar 13 2024 at 15:55):Out of curiosity: could there be an automatic switch to showing sorts or a hint message if the sortless types agree, but the sorts not?
Last updated: May 02 2024 at 04:18 UTC