Is it possible to use a type alias in a GADT definition?

Question

I've been playing around defining a GADT for WebAssembly instructions. Many of these instruction constructors have identical signatures:

data Instruction result where
    Add :: Instruction r -> Instruction r -> Instruction r
    Sub :: Instruction r -> Instruction r -> Instruction r
    Mul :: Instruction r -> Instruction r -> Instruction r

With normal values, you could simply declare a type alias for these binary operators:

type Binop r = Instruction r -> Instruction r -> Instruction r

However, when I use the alias in the GADT definition:

{-# LANGUAGE GADTs #-}

module Data.Instruction where

type Binop r = Instruction r -> Instruction r -> Instruction r

data Instruction result where
    Add :: Binop r
    Sub :: Binop r
    Mul :: Binop r

It fails to compile:

[6 of 6] Compiling Data.Instruction ( src/Data/Instruction.hs, .stack-work/dist/x86_64-osx/Cabal-2.0.1.0/build/Data/Instruction.o )

.../src/Data/Instruction.hs:8:5: error:
    • Data constructor ‘Add’ returns type ‘Binop r’
        instead of an instance of its parent type ‘Instruction result’
    • In the definition of data constructor ‘Add’
      In the data type declaration for ‘Instruction’
   |
11 |     Add :: Binop r
   |     ^

Is there any way to achieve this with GHC? If not, what is the cause of the limitation?

Answer 1

It is possible, but not in the way you've done it. This here does work:

type Foo = Bar Int

data Bar a where
  Bar :: Foo

...because Foo does in fact have the form Bar a, with a ~ Int. However, this doesn't:

type Foo = Int -> Bar Int

data Bar a where
  Bar :: Foo

And it can't work, because the GADT constructor

data Bar a where
  Bar :: Int -> Bar Int

does not actually declare an “invertible function” Bar :: Int -> Bar Int. Rather, it declares something like the following:

data Bar' a = Bar' (a :~: Int) Int

i.e., it encapsulates a (runtime-readable) proof that the a parameter type is in fact Int. The GADT syntax hides this under the hood, but it means you can't just substitute Int -> Bar Int with a type synonym there, because that type synonym would not know how to encapsulate this type-equality proof.

...thinking about it, I'm not sure why my first example actually works, since it would seem to run into the same issue...