[m-dev.] Existentially quantified data constructors

[Mark Brown]

On 15-Apr-2008, Ralph Becket <rafe at csse.unimelb.edu.au> wrote:
> I've defined a type:
> 
> :- type lp_fd_pair(LPSolver, FDSolver)
>     --->    ( some [LPVar, FDVar]
>               lp_fd_pair(LPVar, FDVar)
>               =>    (   flatzinc_solver(LPSolver, LPVar),
>                         flatzinc_solver(FDSolver, FDVar)
>                     )
>             ).
> 
> and received a complaint:
> 
> flatzinc_fdlp_solver.m:093: Error: type variables in class constraints introduced with `=>' must be explicitly existentially quantified using `some': some [_3, _4] lp_fd_pair(_3, _4) => (flatzinc_solver(_1, _3), flatzinc_solver(_2, _4)).
> flatzinc_fdlp_solver.m:321: Error: some but not all arguments have modes: lp_fd_propagator_impl_2(_1, _1, (list(lp_fd_pair) :: in), (is_solved :: out), (pqueue :: di), (pqueue :: uo)).
> 
> Why can't I refer to LPSolver and FDSolver in the type class constraints
> on lp_fd_pair?

Because they are not existentially quantified, and the constraint is
introduced with '=>'.

All constraints have to be either universal (<=), meaning that all type vars
occurring in it are universally quantified, or existential (=>), meaning that
they are all existentially quantified.  You can't have half-half.

If you could, it wouldn't work very well with our implementation: universal
constraints correspond to a typeclass_info with mode `in' (the caller proves
that the constraint is satisfied) and existential constraints the mode is
`out' (the callee proves it).  For a half-half constraint it wouldn't be so
simple.  Where would the typeclass_info go?

Also, I suspect it wouldn't do what you think it might in the above case.

Cheers,
Mark.

--------------------------------------------------------------------------
mercury-developers mailing list
Post messages to:       mercury-developers at csse.unimelb.edu.au
Administrative Queries: owner-mercury-developers at csse.unimelb.edu.au
Subscriptions:          mercury-developers-request at csse.unimelb.edu.au
--------------------------------------------------------------------------