Unable to destroy transitive type

Question

Say I have the following GADT:

data Stage ab where Comb :: Stage ab -> Stage bc -> Stage ac FMap :: (a -> b) -> Stage ab 

Now I want a function that works as follows:

 run (a `Comb` b) = (a,b) run (FMap f) = (FMap f,FMap id) 

How would I build such a function?

I tried different types of type binding, but failed. Is there an extension that I don't have that allows for more extensive type bindings?

This error message is:

 Couldn't match type `t' with `(Stage t1 b, Stage b t2)' `t' is a rigid type variable bound by the inferred type of run :: Stage t1 t2 -> t at <interactive>:11:5 In the expression: (a, b) In an equation for `run': run (a Comb b) = (a, b) 

Description of what I want to execute: I want to create a DSL and run a function that can try to run some DSL code in several ways (I have several different launch functions for each method). The launch function will try to execute as much code as possible provided to it, and then it will tell which code it cannot execute, and what is the result of the code that it could execute.

Answer 1

You will need a type signature for run because you are using a template for GADT. GADT pattern matching requires type refinement and, as a rule, only works if there is a type signature.

But it is unclear what a type signature is. If the input value

 a `Comb` b :: Stage xy 

then you return (a, b) where

 a :: Stage xb b :: Stage by 

for the unknown b . This is an existential type screening. You can not write

 run :: Stage xy -> (State xb, Stage by) 

because it would mean that it should work for all b , but it only works for some (unknown) b .

Unfortunately, it is not clear why you want to write a function like run . Why make a couple? What do you want to do with this pair later? The Comb constructor is defined as combining two stages that have an unknown intermediate type, so this run version will work:

 run :: Stage ab -> Stage ab run (a `Comb` b) = a `Comb` b run (FMap f) = FMap f `Comb` FMap id 

Or you could define a more specific data type, allowing only a “pair” of two steps with an unknown intermediate type:

 data PairStages ab where PairStages :: Stage ab -> Stage bc -> PairStages ac 

And then:

 run :: Stage ab -> PairStages ab run (a `Comb` b) = PairStages ab run (FMap f) = PairStages (FMap f) (FMap id) 

But it still seems strange to me that run returns a pair. As I said, it is not clear what you want to do with the run result. It would seem more useful to have a run recursive function that actually somehow combines the results of starting components in the Comb case. For example, for example:

 run :: Stage ab -> (a -> b) run (a `Comb` b) = run b . run a run (FMap f) = f