I remembered correctly: The wiki talks about it: http://www.impredicative.com/wiki/index.php/Disjointness_fun_-_creating_records_using_type_level_functions quote " Constructing a record type taking two names and two types. Because disjointness can't be proofed at type level it must be done at expression level. "
My goal was to write a type level projection function - but looks like I can't do it for this reason. Marc Weber _______________________________________________ Ur mailing list [email protected] http://www.impredicative.com/cgi-bin/mailman/listinfo/ur
