Haskell: playing with TypeFamilies; could not deduce issue

Question

I am having a play with TypeFamilies and the such in Haskell. I am trying to create a simple example whereby I have a function that takes in some type (Parsers ty) below, and a function that takes a number of arguments dependant on that ty, and outputs some result.

Here's the entire code snippet up front:

{-# LANGUAGE UndecidableInstances, TypeFamilies,GADTs #-}


data V a   --"variable"
data S a   --"static"
data C a b --combination

--define data type:
data Parsers ty where
  ParVar :: a -> Parsers (V a)
  ParStatic :: a -> Parsers (S a)
  ParCombine :: Parsers ty1 -> Parsers ty2 -> Parsers (C ty1 ty2)

--basic type alias to below, output set to Bool
type ExtractVars parsers = GetVars parsers Bool

--we want to convert some combination of C/S/V
--types into a function taking, from left to right,
--each type inside S as parameter
type family GetVars parsers output where
  GetVars (S a) output = output
  GetVars (V a) output = a -> output
  GetVars (C a b) output = GetVars a (GetVars b output)

--this function uses the above such that, hopefully,
--the second argument to be provided will be a function
--that will take each S type as an argument and return
--a bool. We then return that bool from the whole thing
getVars :: Parsers p -> ExtractVars p -> Bool
getVars (ParVar s) fn = fn s
getVars (ParStatic _) fn = fn
-- this is the offending line:
getVars (ParCombine a b) fn = getVars b (getVars a fn)

My Parsers ty type seems to do the right thing; constructing things with it leads to types I would expect eg:

ParVar "hi" 
  :: Parsers (V [Char])
ParCombine (ParVar "hi") (ParStatic "woop")
  :: Parsers (C (V [Char]) (S [Char]))
ParCombine (ParVar 'h') (ParCombine (ParStatic True) (ParVar "hello"))
  :: Parsers (C (V Char) (C (S Bool) (V [Char])))

Equally, my type family GetVars seems to do the right thing, performing conversions such as:

(C (V a) (V b)) out => a -> b -> out
(V a) out           => a -> out
(S a) out           => out
(C (S a) (V b) out  => b -> out

Basically, correctly picking out the things tagged with V in the correct order and ignoring the Ss

My getVars function then uses this in its type signature:

getVars :: Parsers p -> ExtractVars p -> Bool

To say that whatever p is, expect a function matching my type alias ExtractVars p, and return a Bool.

Of my getVars function, these two definitions cause no issue:

getVars (ParVar s) fn = fn s
getVars (ParStatic _) fn = fn

but the final one:

getVars (ParCombine a b) fn = getVars b (getVars a fn)

Fails to typecheck, with the errors:

test.hs:74:42:
    Could not deduce (GetVars ty2 Bool ~ Bool)
    from the context (p ~ C ty1 ty2)
      bound by a pattern with constructor
                 ParCombine :: forall ty1 ty2.
                               Parsers ty1 -> Parsers ty2 -> Parsers (C ty1 ty2),
               in an equation for ‘getVars’
      at test.hs:74:10-23
    Expected type: ExtractVars ty2
      Actual type: Bool
    Relevant bindings include b :: Parsers ty2 (bound at test.hs:74:23)
    In the second argument of ‘getVars’, namely ‘(getVars a fn)’
    In the expression: getVars b (getVars a fn)

test.hs:74:52:
    Could not deduce (GetVars ty1 Bool
                      ~ GetVars ty1 (GetVars ty2 Bool))
    from the context (p ~ C ty1 ty2)
      bound by a pattern with constructor
                 ParCombine :: forall ty1 ty2.
                               Parsers ty1 -> Parsers ty2 -> Parsers (C ty1 ty2),
               in an equation for ‘getVars’
      at test.hs:74:10-23
    NB: ‘GetVars’ is a type function, and may not be injective
    Expected type: ExtractVars ty1
      Actual type: ExtractVars p
    Relevant bindings include
      b :: Parsers ty2 (bound at test.hs:74:23)
      a :: Parsers ty1 (bound at test.hs:74:21)
    In the second argument of ‘getVars’, namely ‘fn’
    In the second argument of ‘getVars’, namely ‘(getVars a fn)’
Failed, modules loaded: none.

(line 74 is the failing ParCombine definition of getVars)

I've been banging my head against the desk trying to figure out where I'm going wrong to no avail, and really want to get a firm grip on the ins and outs of type families as they seem awesome (the above example for instance- being able to expect some function type depending on input - would be incredibly cool!)

Could anyone point my in the right direction or correct my possibly very silly error?

Thanks!

(PS I'm using GHC 7.10.1 and running this in ghci)

Edit Just to say this example was somewhat motivated by a paper on type families, specifically the sprintf example here. Perhaps I have skipped something important in attempting to distill what I wanted from it!

getVars a fn is a Bool but getVars b expects an ExtractVars b — gallais
Usually the answer is "you forgot that type synonym families are not injective" — jberryman
@gallais but isn't the type of getVars a fn is dependant on the type of a here? Eg if a is S a then fn should be a Bool, but if it is V a then fn should be a -> Bool given the type of getVars. — jsdw
@jberryman I believe so. ty here is holding the 'label' (V a, S a or C a b) which depends on the constructor used. I then pass this label to the ExtractVars type alias (and thus GetVars type family) to have it transformed into the function signature I desire. That part, at least, seems to be fine :) — jsdw

András Kovács András Kovács · Accepted Answer · 2015-07-15T20:22:12

Just generalize getVars:

getVars :: Parsers p -> GetVars p out -> out
getVars (ParVar s)       fn = fn s
getVars (ParStatic _)    fn = fn
getVars (ParCombine a b) fn = getVars b (getVars a fn)

With the original type, getVars a fn :: Bool, but we need getVars a fn :: ExtractVars ty2. In general, if we'd like to do substantial computation on GADTs, we must make sure that we have a type general enough so we can actually make the recursive calls (since the types or type indices might change as we recurse).

As a side note, the idiomatic way to represent the GADT indices is to use DataKinds and lifted types:

{-# LANGUAGE DataKinds #-}

data ParserTy a = V a | S a | C (ParserTy a) (ParserTy a)

data Parsers (ty :: ParserTy *) where
  ParVar :: a -> Parsers (V a)
  ParStatic :: a -> Parsers (S a)
  ParCombine :: Parsers ty1 -> Parsers ty2 -> Parsers (C ty1 ty2)

The rest of the code remains the same. This way we can't pollute ParserTy with arbitrary types that don't really belong there, and we can write exhaustive type families over it.

Haskell: playing with TypeFamilies; could not deduce issue

1 Answers