adamc@217: structure M = struct adamc@217: structure N = struct adamc@217: class c t = t adamc@217: val string_c : c string = "Hi" adamc@217: end adamc@217: end adamc@217: adamc@217: val c : t :: Type -> M.N.c t -> t = adamc@217: fn t :: Type => fn pf : M.N.c t => pf adamc@217: val hi = c [string] _ adamc@217: adamc@217: val bool_c : M.N.c bool = True adamc@217: val true = c [bool] _ adamc@217: val hi = c [string] _ adamc@217: adamc@217: con c = M.N.c adamc@217: val int_c : c int = 0 adamc@217: val zero = c [int] _