[Haskell-cafe] Type checking oddity -- maybe my own confusion

[oleg at okmij.org]

Ryan Newton wrote:
> The desired goal was that everywhere I construct a value using the Assign
> constructor, that the resulting value's type to be tainted by the AssignCap
> constraint.

Your code essentially accomplishes the goal:

> data E m where
>   Assign  :: AssignCap m => V -> E m -> E m -> E m
>   Varref  :: V -> E m
> -- ...

Every time you construct the value of the type (E m) with the Assign
constructor, you have to constructively prove -- provide evidence for
-- that the type m is a member of AssignCap. That evidence is stored
within the E m value and so can be reused whenever it is needed later.

Let us modify the example slightly:

> class AssignCap m
> class MutateCap m
>
> data E m where
>   Assign  :: AssignCap m => V -> E m -> E m -> E m
>   Mutate  :: MutateCap m => V -> E m -> E m -> E m
>   Varref  :: V -> E m
> -- ...
>
> type V = String
>
> -- test1 :: E t -> E t
> test1 (Assign v x1 x2) = Assign v x1 x2
>
> -- test2 :: MutateCap t => E t -> E t
> test2 (Assign v x1 x2) = Mutate v x1 x2

To use the constructor Assign, we need the evidence that AssignCap m
holds. The deconstructed value (Assign v x1 x2) provides such an
evidence (as a `hidden' field of the data type). Therefore, the
inferred type for test1 has no constraints. In contrast, in test2 nothing
provides Mutate with the evidence that MutateCap m holds. Therefore,
the inferred type has the MutateCap m constraint.


If storing the evidence is not desired, then one should use ordinary
ADT with smart constructors:

> -- Data constructors should not be exported
> data E1 m = Assign1 V (E1 m) (E1 m) | Varref1 V
> isAssign (Assign1 v x1 x2) = Just (v,x1,x2)
> isAssign _ = Nothing
>
> assign :: AssignCap m => V -> E1 m -> E1 m -> E1 m
> assign = Assign1
>
> -- test3 :: AssignCap m => E1 m -> E1 m
> test3 e | Just (v,x1,x2) <- isAssign e = assign v x1 x2

OCaml has a so-called private constructors, which permit
deconstruction but prohibit construction. They are quite handy,
saving us trouble writing the views like isAssign.

> Actually... to go a bit further, I thought there was some way to arrange
> this so that, upon GHC type-checking the case statement, it would realize
> that certain cases are forbidden based on the type, and would consider the
> pattern match complete without them (or issue an error if they are present).

The key word in the phrase ``certain cases are forbidden based on the
type'' is _type_ -- rather than a type class. If you wish to use this
special GADT feature, you have to `invert' your design. Rather than
specifying what is _required_ to construct an (E m) value, you should
specify what is _provided_.

> data E2 m where
>     Assign2 :: V -> E2 m -> E2 m -> E2 IOT
>     Varref2  :: V -> E2 PureT
>
> test4 :: E2 IOT -> E2 IOT
> test4 (Assign2 v x1 x2) = Assign2 v x1 x2
> test4 (Varref2 _) = undefined

The compiler complaints

    Couldn't match type `IOT' with `PureT'
    Inaccessible code in
      a pattern with constructor
        Varref2 :: V -> E2 PureT,
      in an equation for `test4'
    In the pattern: Varref2 _
    In an equation for `test4': test4 (Varref2 _) = undefined

as desired.