Error with multiple constructors

[RafaelBocquet]

I played a bit with this branch of ghc, and got this strange error :

{-# LANGUAGE GADTs, TypeFamilies, TypeOperators, DataKinds,
             PolyKinds, RankNTypes, ScopedTypeVariables #-}

module A where

data R n = R1 (R n) | R2

-- Typechecks if one of the two constructors is commented
data A i j where
  A1 :: forall n. forall (i :: R n) (j :: R n).
        A i j -> A (R1 i) j
  A2 :: forall n. forall (i :: R n) (j :: R n).
        A i j -> A (R1 i) j

A:hs:13:11
    Expected kind ‘R n’, but ‘i’ has kind ‘R n1’
    In the first argument of ‘A’, namely ‘i’
    In the type ‘A i j’
    In the definition of data constructor ‘A2’

[goldfirere]

Thanks for experimenting!

I think I know what is going on here, and it is indeed a bug. For sanity, let's label the variables to A1 with 1s and those to A2 with 2s.

GHC tries to infer the kind of A. It knows from the declaration that A :: kappa1 -> kappa2 -> *, where kappa1 and kappa2 are unification variables. GHC discovers, looking at A1, that kappa1 ~ R nu1 and kappa2 ~ R nu1, where nu1 :: kappa3. But then, looking at A2, it discovers that kappa1 ~ R nu2 and kappa2 ~ R nu2. However, nu1 and nu2 are user-written quantified variables, so GHC refuses to guess that they are the same.

Another key detail here is that GHC can't generalize A before checking its constructors. If we somehow knew that A :: forall (k :: *) (n :: k). R n -> R n -> *, then we could just supply differing n1 and n2 parameters to the uses of A in the types of A1 and A2. But, GHC can't know A's kind before checking the constructors, so we're in a bind. This detail is all about so-called "Complete User-Specified Kinds", or CUSKs: if GHC can be sure of a type's exact kind before looking at its constructors, then it will generalize the type before continuing. (This behavior exists in GHC today. See GHC#9200 for much discussion.)

How to solve this? GHC has an internal way of saying that it's OK to unify one user-written quantified variable with another. (These are known as SigTyVars.) Perhaps we could make the ns SigTyVars, and then n1 will unify with n2, and all will be well. But is this always safe? I'm not sure, off the top of my head.

It's possible that we'll need to differentiate arguments from parameters here, much like proper dependently typed languages do in inductive datatype definitions. In other words, require in the data declaration head to separate n -- which is the same at every use site in the constructors -- from i and j (because i differs).

In any case, great example. Thanks.