Oops, I forgot to mention before, are these still needed?  I think default implicit arguments are different for `Class` vs `Record`.  If you keep this and the comment, `hproptype`, `isp` -> `[hproptype]`, `[isp]` in the comment.  Also, the `Coercion` can be done by replacing `hproptype : Type` with `hproptype :> Type`, now that it's a `Record` rather than a `Class`.  (It's somewhat confusing that `:>` means `Existing Instance` for `Class`, but `Coercion` for `Record`.)