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

Question

I am defining GADT instructions for WebAssembly. Many of these command 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 can simply declare a type alias for these binary operators:

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

However, when I use an 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

Unable 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 using the GHC? If not, what is the reason for the restriction?

Answer 1

Maybe <but not the way you did it. It works:

type Foo = Bar Int

data Bar a where
  Bar :: Foo

... because it Fooreally has the form Bar a, p a ~ Int. However, it is not:

type Foo = Int -> Bar Int

data Bar a where
  Bar :: Foo

And it cannot work because the GADT constructor

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

" " Bar :: Int -> Bar Int. , :

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

i.e., ( ) , a Int. GADT , , Int -> Bar Int , , .

... , , , , , ...