Basic Haskell monomorphism/polymorphism question (HList)

Question

I'm a Haskell and a Stackoverflow noob, and here's my first & probably quite basic Haskell question.

module M where

import Data.HList

data R r a 

r1 = undefined :: R a Int
r2 = undefined :: R a Double

rPair :: R r a -> R r b -> (R r a, R r b)
rPair = (,)

rp = rPair r1 r2

This makes sense, even if r1 & r2 are polymorphic in r rPair aligns their r type in accordance with the type signature. Is there a technical term for this 'alignment'?

class HList l => RList r l
instance RList r HNil
instance RList r l => RList r (HCons (R r a) l)

rCons :: RList r l => R r a -> l -> (HCons (R r a) l)
rCons = hCons

rc = rCons r1 (rCons r2 hNil)

rCons works great if the R's passed are monomorphic in r, constraining the list's r type as desired. but if they are polymorphic in r it does not align them the way rPair does, and gives an error (defining rc above).

No instance for (RList r (HCons (R r1 Double) HNil))

I have a vague intuition as to why this is the case, but my question is in two parts. Could somebody clearly explain the phenomenon? How would I write an rCons such that the following would hold?

r1 = undefined :: R a Int
r2 = undefined :: R a Double

rc :: HCons (R a Int) (HCons (R a Double) HNil)
rc = rCons r1 (rCons r2 hNil)

Thanks, _c

Answer 1

To answer your second question, you can use type equivalence constraint (from TypeFamilies extension) to relax your RList instance definition:

class HList l => RList r l
instance RList r HNil
instance (RList r1 l, r1 ~ r2) => RList r1 (HCons (R r2 a) l)

Now your rc will be inferred to the desired type.

I don't think I can 'clearly explain' the phenomenon though (somebody surely will), but it's obvious that the difference between rPair and rCons is that while the former binds r type of both arguments to the same type variable, the later doesn't: the second argument is just l constrained with that there should be some instance of RList for that l). Since there is no type signature for rc (note that if you provide one your original example typechecks) and r1 and r2 have polymorphic, not equivalent, r's , compiler is trying to find an instance definition for RList r (HCons (R r1 Double) HNil) (r comes from the 1st argument and r1 - from the 2nd) and fails to do so. With type equivalence constraint we define an instance of RList with two distinct r1 and r2 with the only condition that these needs to be equivalent, so it looks like GHC binds them to the same polymorphic type variable when resolving instance of RList for l.