Signature Item Typing

We appeal to a signature item analogue of the $\mathcal O$ function from the last subsection.

This is the first judgment where we deal with constructor classes, for the $\mathsf{class}$ forms. We will omit their special handling in this formal specification. Section 6.3 gives an informal description of how constructor classes influence type inference.

$$\infer{\Gamma \vdash \cdot \leadsto \Gamma}{} \quad \infer{\Gamma... ...ma \vdash s \leadsto \Gamma' & \Gamma' \vdash \overline{s} \leadsto \Gamma'' }$$

$$\infer{\Gamma \vdash \mathsf{con} \; x :: \kappa \leadsto \Gamma,... ...sf{len}(\overline y)} \to \mathsf{Type} \vdash \overline{dc} \leadsto \Gamma' }$$

$$\infer{\Gamma \vdash \mathsf{datatype} \; x = \mathsf{datatype} \... ...}(\overline y)} \to \mathsf{Type} = M.z \vdash \overline{dc} \leadsto \Gamma' }$$

$$\infer{\Gamma \vdash \mathsf{val} \; x : \tau \leadsto \Gamma, x : \tau}{ \Gamma \vdash \tau :: \mathsf{Type} }$$

$$\infer{\Gamma \vdash \mathsf{structure} \; X : S \leadsto \Gamma,... ... \vdash \mathsf{signature} \; X = S \leadsto \Gamma, X = S}{ \Gamma \vdash S }$$

$$\infer{\Gamma \vdash \mathsf{include} \; S \leadsto \Gamma, \math... ...dash S & \Gamma \vdash S \equiv \mathsf{sig} \; \overline{s} \; \mathsf{end} }$$

$$\infer{\Gamma \vdash \mathsf{constraint} \; c_1 \sim c_2 \leadsto... ...sim c_2}{ \Gamma \vdash c_1 :: \{\kappa\} & \Gamma \vdash c_2 :: \{\kappa\} }$$

$$\infer{\Gamma \vdash \mathsf{class} \; x :: \kappa = c \leadsto \... ...fer{\Gamma \vdash \mathsf{class} \; x :: \kappa \leadsto \Gamma, x :: \kappa}{}$$