On 2013-06-20 20:49, Sergei Meshveliani wrote: > Is it possible to add some construct foo to the language so that the > checker would allow to replace f : PSSmg a with f : PSSmg b, if p : > associated a b and foo is set for PSSmg ? I didn't read all of your question, but I think you're looking for something like quotients. -- /NAD