GADTs preventing me from making an amazing parser library

Learn
1

I can’t figure out how to fix this. I would have thought it could tell that both the pattern from the Call constructor and the pattern from the Lambda constructor were true at the same time since one is inside the other. I ‘just’ want it to copy the value u out of frame f into frame g, run the body, and then copy the return value v out of frame g into frame f. Is this possible? It seems to be GADTs getting in my way, and I don’t really understand them. The whole thing is on GitHub. And also a parser using it for editing mp3 ID3 metadata It uses one specification to both parse and format for saving the edited mp3s. I’ve got this

class Frame name value frame where
   myget1 :: name -> frame -> value
   myset1 :: name -> value -> frame -> frame

data Rule s t f r where
  Call   :: (Frame m u f, Frame n v f) => m -> Lambda s t g u v -> n -> Rule s t f  v

data Lambda s t g u v where
  Lambda :: (Frame j u g, Frame k v g) => j -> Rule s t g v -> k -> Lambda s t g u v

parse1 :: (Show str, BStringC tok str, Eq tok, Show tok, Ord tok) => Rule str tok frame res -> frame -> str -> IResult str tok frame res

... other clauses of parse1 ...

parse1 (Call m (Lambda j body k) n) f t =
  case parse1 body (myset1 j (myget1 m f) undefined) t of
    Done t1 g r1 -> Done t1 (myset1 n (myget1 k g) f) r1

... other clauses of parse1 ...

giving these errors:

• Could not deduce ‘Frame j value0 g’
    arising from a use of ‘myset1’
  from the context: (Show str, BStringC tok str, Show tok, Ord tok)
    bound by the type signature for:
               parse1 :: forall str tok frame res.
                         (Show str, BStringC tok str, Eq tok, Show tok, Ord tok) =>
                         Rule str tok frame res -> frame -> str -> IResult str tok frame res
    at /home/brett/swissarmyknife/Parser5.hs:229:1-136
  or from: (Frame m u frame, Frame n res frame)
    bound by a pattern with constructor:
               Call :: forall m u f n v s t g.
                       (Frame m u f, Frame n v f) =>
                       m -> Lambda s t g u v -> n -> Rule s t f v,
             in an equation for ‘parse1’
    at /home/brett/swissarmyknife/Parser5.hs:349:9-34
  or from: (Frame j u g, Frame k res g)
    bound by a pattern with constructor:
               Lambda :: forall j u g k v s t.
                         (Frame j u g, Frame k v g) =>
                         j -> Rule s t g v -> k -> Lambda s t g u v,
             in an equation for ‘parse1’
    at /home/brett/swissarmyknife/Parser5.hs:349:17-31
  The type variable ‘value0’ is ambiguous
  Relevant bindings include
    body :: Rule str tok g res
      (bound at /home/brett/swissarmyknife/Parser5.hs:349:26)
    j :: j (bound at /home/brett/swissarmyknife/Parser5.hs:349:24)
• In the second argument of ‘parse1’, namely
    ‘(myset1 j (myget1 m f) undefined)’
  In the expression: parse1 body (myset1 j (myget1 m f) undefined) t
  In the expression:
    case parse1 body (myset1 j (myget1 m f) undefined) t of
      Done t1 g r1 -> Done t1 (myset1 n (myget1 k g) f) r1

and

• Could not deduce ‘Frame m value0 frame’
    arising from a use of ‘myget1’
  from the context: (Show str, BStringC tok str, Show tok, Ord tok)
    bound by the type signature for:
               parse1 :: forall str tok frame res.
                         (Show str, BStringC tok str, Eq tok, Show tok, Ord tok) =>
                         Rule str tok frame res -> frame -> str -> IResult str tok frame res
    at /home/brett/swissarmyknife/Parser5.hs:229:1-136
  or from: (Frame m u frame, Frame n res frame)
    bound by a pattern with constructor:
               Call :: forall m u f n v s t g.
                       (Frame m u f, Frame n v f) =>
                       m -> Lambda s t g u v -> n -> Rule s t f v,
             in an equation for ‘parse1’
    at /home/brett/swissarmyknife/Parser5.hs:349:9-34
  or from: (Frame j u g, Frame k res g)
    bound by a pattern with constructor:
               Lambda :: forall j u g k v s t.
                         (Frame j u g, Frame k v g) =>
                         j -> Rule s t g v -> k -> Lambda s t g u v,
             in an equation for ‘parse1’
    at /home/brett/swissarmyknife/Parser5.hs:349:17-31
  The type variable ‘value0’ is ambiguous
  Relevant bindings include
    f :: frame (bound at /home/brett/swissarmyknife/Parser5.hs:349:37)
    m :: m (bound at /home/brett/swissarmyknife/Parser5.hs:349:14)
    parse1 :: Rule str tok frame res
              -> frame -> str -> IResult str tok frame res
      (bound at /home/brett/swissarmyknife/Parser5.hs:230:1)
• In the second argument of ‘myset1’, namely ‘(myget1 m f)’
  In the second argument of ‘parse1’, namely
    ‘(myset1 j (myget1 m f) undefined)’
  In the expression: parse1 body (myset1 j (myget1 m f) undefined) t

and

• Could not deduce ‘Frame n value1 frame’
    arising from a use of ‘myset1’
  from the context: (Show str, BStringC tok str, Show tok, Ord tok)
    bound by the type signature for:
               parse1 :: forall str tok frame res.
                         (Show str, BStringC tok str, Eq tok, Show tok, Ord tok) =>
                         Rule str tok frame res -> frame -> str -> IResult str tok frame res
    at /home/brett/swissarmyknife/Parser5.hs:229:1-136
  or from: (Frame m u frame, Frame n res frame)
    bound by a pattern with constructor:
               Call :: forall m u f n v s t g.
                       (Frame m u f, Frame n v f) =>
                       m -> Lambda s t g u v -> n -> Rule s t f v,
             in an equation for ‘parse1’
    at /home/brett/swissarmyknife/Parser5.hs:349:9-34
  or from: (Frame j u g, Frame k res g)
    bound by a pattern with constructor:
               Lambda :: forall j u g k v s t.
                         (Frame j u g, Frame k v g) =>
                         j -> Rule s t g v -> k -> Lambda s t g u v,
             in an equation for ‘parse1’
    at /home/brett/swissarmyknife/Parser5.hs:349:17-31
  The type variable ‘value1’ is ambiguous
  Relevant bindings include
    f :: frame (bound at /home/brett/swissarmyknife/Parser5.hs:349:37)
    n :: n (bound at /home/brett/swissarmyknife/Parser5.hs:349:34)
    parse1 :: Rule str tok frame res
              -> frame -> str -> IResult str tok frame res
      (bound at /home/brett/swissarmyknife/Parser5.hs:230:1)
• In the second argument of ‘Done’, namely
    ‘(myset1 n (myget1 k g) f)’
  In the expression: Done t1 (myset1 n (myget1 k g) f) r1
  In a case alternative:
      Done t1 g r1 -> Done t1 (myset1 n (myget1 k g) f) r1

and

• Could not deduce ‘Frame k value1 g’
    arising from a use of ‘myget1’
  from the context: (Show str, BStringC tok str, Show tok, Ord tok)
    bound by the type signature for:
               parse1 :: forall str tok frame res.
                         (Show str, BStringC tok str, Eq tok, Show tok, Ord tok) =>
                         Rule str tok frame res -> frame -> str -> IResult str tok frame res
    at /home/brett/swissarmyknife/Parser5.hs:229:1-136
  or from: (Frame m u frame, Frame n res frame)
    bound by a pattern with constructor:
               Call :: forall m u f n v s t g.
                       (Frame m u f, Frame n v f) =>
                       m -> Lambda s t g u v -> n -> Rule s t f v,
             in an equation for ‘parse1’
    at /home/brett/swissarmyknife/Parser5.hs:349:9-34
  or from: (Frame j u g, Frame k res g)
    bound by a pattern with constructor:
               Lambda :: forall j u g k v s t.
                         (Frame j u g, Frame k v g) =>
                         j -> Rule s t g v -> k -> Lambda s t g u v,
             in an equation for ‘parse1’
    at /home/brett/swissarmyknife/Parser5.hs:349:17-31
  The type variable ‘value1’ is ambiguous
  Relevant bindings include
    g :: g (bound at /home/brett/swissarmyknife/Parser5.hs:351:15)
    k :: k (bound at /home/brett/swissarmyknife/Parser5.hs:349:31)
    body :: Rule str tok g res
      (bound at /home/brett/swissarmyknife/Parser5.hs:349:26)
• In the second argument of ‘myset1’, namely ‘(myget1 k g)’
  In the second argument of ‘Done’, namely
    ‘(myset1 n (myget1 k g) f)’
  In the expression: Done t1 (myset1 n (myget1 k g) f) r1
1 Like
2

I made it simpler. I think this more simply expresses what I want to do

class Frame name value frame where
   lookup :: name -> frame -> value
   update :: name -> value -> frame -> frame

data Rule s t f i o where
   Call    :: (Frame m u f, Frame n v f) => m -> Rule s t g u v -> n -> Rule s t f u v
   Lambda  :: (Frame j u g, Frame k v g) => j -> Rule s t g u v -> k -> Rule s t g u v
   IsoRule :: (a -> b) -> (b -> a) -> Rule s t f a b

data PResult t f r = Done t f r

parse1 (Call m (Lambda j body k) n) f t =
   case parse1 body (update j (lookup m f) undefined) t of
      Done t1 g r1 -> Done t1 (update n (lookup k g) f) r1

Parser2.hs:52:9: error: [GHC-25897]
    • Couldn't match type ‘g’ with ‘f’
      Expected: Rule s t1 g i o -> frame -> p -> PResult t2 frame r
        Actual: Rule s t1 f i o -> frame -> p -> PResult t2 frame r
      ‘g’ is a rigid type variable bound by
        a pattern with constructor:
          Call :: forall {k1} {k2} m u f n v (s :: k1) (t :: k2) g.
                  (Frame m u f, Frame n v f) =>
                  m -> Rule s t g u v -> n -> Rule s t f u v,
        in an equation for ‘parse1’
        at Parser2.hs:51:9-34
      ‘f’ is a rigid type variable bound by
        the inferred type of
          parse1 :: Rule s t1 f i o -> frame -> p -> PResult t2 frame r
        at Parser2.hs:(51,1)-(53,58)
    • In the expression:
        parse1 body (update j (lookup m f) undefined) t
      In the expression:
        case parse1 body (update j (lookup m f) undefined) t of
          Done t1 g r1 -> Done t1 (update n (lookup k g) f) r1
      In an equation for ‘parse1’:
          parse1 (Call m (Lambda j body k) n) f t
            = case parse1 body (update j (lookup m f) undefined) t of
                Done t1 g r1 -> Done t1 (update n (lookup k g) f) r1
    • Relevant bindings include
        body :: Rule s t1 g i o (bound at Parser2.hs:51:26)
        parse1 :: Rule s t1 f i o -> frame -> p -> PResult t2 frame r
          (bound at Parser2.hs:51:1)
   |
52 |    case parse1 body (update j (lookup m f) undefined) t of
   |         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
3

It seems to not like the fact that the Call type signature has a Rule s t g u v as the 2nd param but a result type of Rule s t f u v, therefore leaving it unable to figure out what g is. Can GHC not figure out (because the Lambda is inside the Call), what the type of g is? Is there some way of me telling it through annotations, that still allow GADTs?

4

If I give it a clue what g is, we’re back to the original four errors

class Frame name value frame where
   lookup :: name -> frame -> value
   update :: name -> value -> frame -> frame

data Rule s t f i o where
   Call    :: (Frame m u f, Frame n v f) => m -> g -> Rule s t g u v -> n -> Rule s t f u v
   Lambda  :: (Frame j u g, Frame k v g) => j -> Rule s t g u v -> k -> Rule s t g u v
   IsoRule :: Iso a b -> Rule s t f a b

data PResult s f r = Done s f r

parse1 :: Rule s t f i o -> f -> s -> PResult s f r
parse1 (Call m g (Lambda j body k) n) f t =
   case parse1 body (update j (lookup m f) g) t of
      Done t1 g1 r1 -> Done t1 (update n (lookup k g1) f) r1
5

The key part of the error message is:

The type variable ‘value0’ is ambiguous

So you were on to something here:

[…] leaving it unable to figure out what g is. […] Is there some way of me telling it through annotations […]?

Except that g isn’t the problem. It’s i and o.

One possible solution using type applications:

parse1 :: forall s t f i o r. Rule s t f i o -> f -> s -> PResult s f r
parse1 (Call m g (Lambda j body k) n) f t =
    case parse1 body (update @_ @i j (lookup m f) g) t of
        Done t1 g1 r1 -> Done t1 (update @_ @o n (lookup k g1) f) r1
1 Like
6

Thanks. I’ve done what you said (and fixed a few other things) but it’s now complaining about type variables i and o not being in scope

{-# LANGUAGE TypeApplications #-}

class Frame name value frame where
   lookup :: name -> frame -> value
   update :: name -> value -> frame -> frame

data Rule s t f i o where
   Call    :: (Frame m u f, Frame n v f) => m -> Rule s t g u v -> n -> Rule s t f u v
   Lambda  :: (Frame j u g, Frame k v g) => j -> Rule s t g u v -> k -> Rule s t g u v
   IsoRule :: (a -> b) -> (b -> a) -> Rule s t f a b

data PResult s f o = Done s f o

parse1 :: Rule s t f i o -> f -> s -> i -> PResult s f o
parse1 (Call m (Lambda j body k) n) f s i  =
   case parse1 body (update @_ @i j (lookup m f) undefined) s i of
      Done s1 g1 r1 -> Done s1 (update @_ @o n (lookup k g1) f) r1

Not in scope: type variable ‘i’
Not in scope: type variable ‘o’
7

You need the explicit forall I used, in order to bring the type variables in to scope.

8

That seems to have fixed it. Cheers

1 Like
9

If it’s fixed, you should change the category to learn and mark it as solved.

1 Like