Record Foo := MkFoo { field1 : nat; field2 : nat -> nat }.

Canonical Structure Foo.