AST Thinning

So we've discussed quite a bit about how we can reduce the number AST constructors that need to be matched on at various stages of the compilation pipeline by "thinning". I've been playing around with different ways of doing this and I thought I should share them with everyone, so we can decide which representation we want.

Firstly, this is one that should work, but unfortunately doesn't. If we define the stages of our compilation like so:

``` haskell
data Stage = HigherOrder | FirstOrder | Fused
```

Where `HigherOrder` is the earliest stage before any transformation, `FirstOrder` is after vectorisation and prior to fusion, and `Fused` is after fusion (all of this is under the assumption that we may want to have more stages in future). We can then define a type-level ordering on stages.

``` haskell
type family (s1 :: Stage) $<= (s2 :: Stage) where
HigherOrder $<= HigherOrder = (True ~ True)
FirstOrder $<= FirstOrder = (True ~ True)
Fused $<= Fused = (True ~ True)
HigherOrder $<= FirstOrder = (True ~ True)
HigherOrder $<= Fused = (True ~ True)
FirstOrder $<= Fused = (True ~ True)
a $<= b = (True ~ False)
```

GHC currently doesn't have a nice type for just a satisfiable or non-satisfiable constraint, hence the whole `True ~ True` and `True ~ False` stuff. We could easily define our own though.

Here's a highly simplified version of the AST with stage annotations.

``` haskell
data PreOpenAcc acc stage env a where
Map :: PreOpenFun acc stage env (a -> b)
-> acc stage env (Array sh a)
-> PreOpenAcc acc stage env (Array sh b)

ZipWith :: (stage $<= FirstOrder)
=> PreOpenFun acc stage env (a -> b -> c)
-> acc stage env a
-> acc stage env b
-> PreOpenAcc acc stage env c

Apply :: PreOpenAfun acc stage env (a -> b)
-> acc stage env a
-> PreOpenAcc acc stage env b

data OpenAcc stage env a = OpenAcc (PreOpenAcc OpenAcc stage env a)

data PreOpenAfun acc stage env f where
Abody :: acc stage env f -> PreOpenAfun acc stage env f
Alam :: PreOpenAfun acc stage (env,a) f -> PreOpenAfun acc stage env (a -> f)
AlamVar :: Idx env f -> PreOpenAfun acc HigherOrder env f
```

You can see how we've used the ordering on stages to assert that `ZipWith` only occurs in stages prior to and including `FirstOrder` and that higher order functions are only expressible in the `HigherOrder` stage.

The problem occurs when we try to write a traversal over the AST. For example, say we want to to a traversal that only works over the `Fused` stage syntax:

``` haskell
someTraversal :: OpenAcc Fused env a -> String
someTraversal (OpenAcc a) = trav a
where
trav :: PreOpenAcc OpenAcc Fused env a -> String
trav (Map _ _) = "map"
trav (Apply _ _) = "apply"
```

GHC is unable to determine that we don't need to match on `ZipWith`, so it raises a warning. However, if we do match on `Zipwith`, it is smart enough to see it shouldn't be there and gives an inaccesible code error, regardless of what's on the RHS. This is a known bug in GHC (https://ghc.haskell.org/trac/ghc/ticket/3927) and AFAIK it will not be fixed in 7.10. The only "solution" is to have this.

``` haskell
trav _ = error "Unreachable code"
```

This obviously just makes matter worse if we ever try to add more operations to the AST.

I tried a few variations on this solution, but they all had this same problem. GHC is not able to see impossible constraints when doing its pattern incompleteness checks.

The other solution, that does work, is instead of stages we have a set of properties. Just for starters, it might look like this.

``` haskell
data Properties = P Bool -- ^ Is higher order?
Bool -- ^ Has fusable operations?
```

Our stages are then

``` haskell
type Fused = P False False
type FirstOrder = P False True
type HigherOrder = P True True
```

And our annotated AST is

``` haskell
data PreOpenAcc acc props env a where
Map :: PreOpenFun acc props env (a -> b)
-> acc props env (Array sh a)
-> PreOpenAcc acc props env (Array sh b)

ZipWith :: PreOpenFun acc (P ho True) env (a -> b -> c)
-> acc (P ho True) env a
-> acc (P ho True) env b
-> PreOpenAcc acc (P ho True) env c

Apply :: PreOpenAfun acc props env (a -> b)
-> acc props env a
-> PreOpenAcc acc props env b

data OpenAcc props env a = OpenAcc (PreOpenAcc OpenAcc props env a)

data PreOpenAfun acc props env f where
Abody :: acc props env f -> PreOpenAfun acc props env f
Alam :: PreOpenAfun acc props (env,a) f -> PreOpenAfun acc props env (a -> f)
AlamVar :: Idx env f -> PreOpenAfun acc (P True zw) env f
```

Doing it this way means `someTraversal` now works without spitting out a warning about not matching on `ZipWith`.

The disadvantage of this approach is that it is quite verbose, especially if we add more properties. We also probably want to get rid of the opaque `Bool`s and replace them with something like this.

``` haskell
data IsHigherOrder = YesHigherOrder | NoHigherOrder
```

This would also add to the verbosity.

What does everyone think?

Other issues that also need to be considered are:
- The need for a separate `PreOpenAfun` data type. Could we not just add `Alam` to `PreOpenAcc`?
- Whether we should do what we've talked about for a while: Add something like `PrimApp` to `PreOpenAcc` and putting all of the operations in `PrimAfun`. I like this idea because it separates the operations of the language from the general structure, meaning that, for example, Substitution.hs could be drastically reduced in size. This would be a LOT of work.
- How should we introduce this, all at once or should we keep both versions of the syntax around and have conversions between them until we've completed the whole change?

I've got all the code [here](https://gist.github.com/robeverest/5b1e66eebcbde9827a33), in case anyone else wants to play around with it.