# HG changeset patch # User huffman # Date 1287606150 25200 # Node ID 3007608368e29c326a4759ddcb5965477f070b55 # Parent 87c72a02eaf228e67e9d41ed493207623f15b5d4 constructor arguments with selectors must have pointed types diff -r 87c72a02eaf2 -r 3007608368e2 src/HOLCF/Tools/Domain/domain.ML --- a/src/HOLCF/Tools/Domain/domain.ML Wed Oct 20 13:02:13 2010 -0700 +++ b/src/HOLCF/Tools/Domain/domain.ML Wed Oct 20 13:22:30 2010 -0700 @@ -106,15 +106,17 @@ quote (Syntax.string_of_typ_global thy t) ^ " with different arguments")) | analyse indirect (TVar _) = error "extender:analyse"; - fun check_pcpo lazy T = - let val sort = arg_sort lazy in + (* a lazy argument may have an unpointed type *) + (* unless the argument has a selector function *) + fun check_pcpo sel lazy T = + let val sort = arg_sort (lazy andalso is_none sel) in if Sign.of_sort thy (T, sort) then T else error ("Constructor argument type is not of sort " ^ Syntax.string_of_sort_global thy sort ^ ": " ^ Syntax.string_of_typ_global thy T) end; fun analyse_arg (lazy, sel, T) = - (lazy, sel, check_pcpo lazy (analyse false T)); + (lazy, sel, check_pcpo sel lazy (analyse false T)); fun analyse_con (b, args, mx) = (b, map analyse_arg args, mx); in map analyse_con cons' end; in ListPair.map analyse_equation (dtnvs,cons'')