How to type function which takes arguments of a DataKind indexed type instantiated with different indices?

Question

I want to have a data type which contains booleans and doubles strictly in an alternating fashion. Like this:

tw0 = TWInit True
tw1 = TWInit True :-- 0.5
tw2 = TWInit True :-- 0.5 :- False
tw3 = TWInit True :-- 0.5 :- False :-- 0.5

With the following code, all of the above can be typed:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PatternSynonyms #-}

data TWEnd = TWESample | TWETime

data TimedWord (end :: TWEnd) where
  TWInit :: Bool -> TimedWord 'TWESample
  TWTime :: TimedWord 'TWESample -> Double -> TimedWord 'TWETime
  TWSample :: TimedWord 'TWETime -> Bool -> TimedWord 'TWESample

pattern (:--) :: TimedWord 'TWESample -> Double -> TimedWord 'TWETime
pattern t :-- x = TWTime t x

pattern (:-) :: TimedWord 'TWETime -> Bool -> TimedWord 'TWESample
pattern t :- s = TWSample t s

However, it is not clear to me how to type something like this:

printTimedWord (TWInit sample) = "TWInit " ++ show sample
printTimedWord (tw :-- x) = printTimedWord tw ++ " :-- " ++ show x
printTimedWord (tw :- sample) = printTimedWord tw ++ " :- " ++ show sample

Haskell does not seem to like the above definition because the first argument is both of type TimedWord TWETime and TimedWord TWESample. How can I fix this?

Answer 1

If you have a TimedWord end (for some unknown type variable end), then pattern matching on the GADT constructors just works (an explicit type signature is necessary though):

printTimedWord :: TimedWord end -> String
printTimedWord (TWInit sample) = "TWInit " ++ show sample
printTimedWord (TWTime tw x) = printTimedWord tw ++ " :-- " ++ show x
printTimedWord (TWSample tw sample) = printTimedWord tw ++ " :- " ++ show sample

So your problem is not "how to accept GADTs with different type indexes", but rather that it seems pattern synonyms don't play nicely with this GADT feature. I'm not sure if it's impossible to write pattern synonyms that work like GADT constructors, or whether there's just something extra you have to do.

However it seems (at least from your simple example) that you simply would rather use infix operators than named constructors? So an alternative way to fix your problem is to ditch the pattern synonyms and simply use :-- and :- as the constructors in the first place:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PatternSynonyms #-}

data TWEnd = TWESample | TWETime

data TimedWord (end :: TWEnd) where
  TWInit :: Bool -> TimedWord 'TWESample
  (:--) :: TimedWord 'TWESample -> Double -> TimedWord 'TWETime
  (:-) :: TimedWord 'TWETime -> Bool -> TimedWord 'TWESample

printTimedWord :: TimedWord end -> String
printTimedWord (TWInit sample) = "TWInit " ++ show sample
printTimedWord (tw :-- x) = printTimedWord tw ++ " :-- " ++ show x
printTimedWord (tw :- sample) = printTimedWord tw ++ " :- " ++ show sample

---

I know this is unlikely to be your entire problem, but if you use the operators as the real constructors and provide infix declarations for them, then GHC can simply derive a Show instance for you that basically matches what you're trying to do with printTimedWord (but requires StandaloneDeriving, if you're not using GHC2021):

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE StandaloneDeriving #-}

data TWEnd = TWESample | TWETime

data TimedWord (end :: TWEnd) where
  TWInit :: Bool -> TimedWord 'TWESample
  (:--) :: TimedWord 'TWESample -> Double -> TimedWord 'TWETime
  (:-) :: TimedWord 'TWETime -> Bool -> TimedWord 'TWESample

printTimedWord :: TimedWord end -> String
printTimedWord (TWInit sample) = "TWInit " ++ show sample
printTimedWord (tw :-- x) = printTimedWord tw ++ " :-- " ++ show x
printTimedWord (tw :- sample) = printTimedWord tw ++ " :- " ++ show sample

infixr 8 :-
infixr 8 :--
deriving instance Show (TimedWord end)

With this we can see:

λ printTimedWord $ (TWInit True) :-- 3
"TWInit True :-- 3.0"

λ show $ (TWInit True) :-- 3
"TWInit True :-- 3.0"

So you don't necessarily need to implement printTimedWord at all.

(I have no idea what associativity or precedence is actually appropriate, I just picked something arbitrarily; with no infix declarations the derived Show instance prints the constructors in prefix form like (:--) (TWInit True) 3.0. Infix declarations are probably a good idea regardless though, whether they're pattern synonyms or real constructors)

Answer 2

I don't really see any reason why you'd use pattern synonyms here; in doubt I'd always just use the GADT constructor as in Ben's answer.

That said, here's how to do it with pattern synonyms:

pattern (:%) :: () => (end ~ 'TWETime)
    => TimedWord 'TWESample -> Double -> TimedWord end
pattern t :% x = TWTime t x

pattern (:-) :: () => (end ~ 'TWESample)
    => TimedWord 'TWETime -> Bool -> TimedWord end
pattern t :- s = TWSample t s

printTimedWord :: TimedWord end -> String
printTimedWord (TWInit sample) = "TWInit " ++ show sample
printTimedWord (tw :% x) = printTimedWord tw ++ " :% " ++ show x
printTimedWord (tw :- sample) = printTimedWord tw ++ " :- " ++ show sample

The trick is to have the end ~ 'TWESample constraint not in the "required" position, but in the "provided" position of the synonyms' signature. Cf. pattern synonyms / static semantics.