TyFam inductive case

rightComb.hs

import Data.Vinyl (Rec(..))

data Tag = TagInt | TagPair Tag Tag

data Exp (t :: Tag) where
  EInt :: Int -> Exp 'TagInt
  EPair :: Exp t1 -> Exp t2 -> Exp ('TagPair t1 t2)

type family RightComb (tags :: [Tag]) :: Tag where
  RightComb '[ x, y ] = 'TagPair x y
  RightComb (x ': xs) = 'TagPair x (RightComb xs)

-- Turns:
--    EInt 1 :& EInt 2 :& EInt 3 :& RNil
-- Into:
--    EPair (EInt 1) (EPair (EInt 2) (EInt 3))
rightComb :: forall (tags :: [Tag]) . Rec Exp tags -> Exp (RightComb tags)
rightComb = \case
  a :& b :& RNil -> EPair a b
  a :& xs -> EPair a (rightComb xs)

x_error.md

• Could not deduce: RightComb (r : rs) ~ 'TagPair r (RightComb rs)
      from the context: input ~ (r : rs)
        bound by a pattern with constructor:
                   :& :: forall u (a :: u -> *) (r :: u) (rs :: [u]).
                         a r -> Rec a rs -> Rec a (r : rs),
                 in a case alternative
        at src/Michelson/Example.hs:18:3-9
      Expected type: Exp (RightComb input)
        Actual type: Exp ('TagPair r (RightComb rs))
    • In the expression: EPair a (rightComb xs)
      In a case alternative: a :& xs -> EPair a (rightComb xs)
      In the expression:
        \case
          a :& b :& RNil -> EPair a b
          a :& xs -> EPair a (rightComb xs)
    • Relevant bindings include
        xs :: Rec Exp rs (bound at src/Michelson/Example.hs:18:8)
        a :: Exp r (bound at src/Michelson/Example.hs:18:3)
   |
18 |   a :& xs -> EPair a (rightComb xs)
   |              ^^^^^^^^^^^^^^^^^^^^^^

Update: this works:

type family RightComb (tags :: [Tag]) :: Tag where
  RightComb '[ x ] = x
  RightComb (x ': xs) = 'TagPair x (RightComb xs)

rightComb :: forall (tags :: [Tag]) . Rec Exp tags -> Exp (RightComb tags)
rightComb = \case
  a :& RNil -> a
  a :& b :& xs -> EPair a (rightComb (b :& xs))
```