GADTs by themselves do not allow arbitrary computation[1]. But Haskell also allows you to write functions at the type-level ("type families" in the Haskell jargon), so you can directly write functions to compute types without any trickery, and the Propeller example uses this feature.
GADTs let you write down basically the same things that you could write as an inductive datatype in a dependent language like Coq and Agda. So (with some patience) you can make a function return a "proof" of anything that can be witnessed by a first-order inductive type, e.g. equations between expressions, list membership, proofs that a term in an object-language is welltyped, etc. The main limitation is that Haskell doesn't have any termination checking, so if you consider it as a dependently typed language there is no way to write a trustworthy proof that uses induction. Also its not very user-friendly, see [2] for some examples.
[1] Basically, GADTs are equivalent to having equations between types. If all the equations are written out in full, it is reasonably straightforward to check whether two types are provably equal. If you want to do type _inference_, i.e. figure out what equality assumptions a given function should make in order to become welltyped, then you run into various undecidable problems (e.g. "rigid E-unification"). My guess would be that if you wrote down a completely general typesystem featuring GADTs, then you would be able to encode arbitrary computations as type-inference problems, but the encoding would be very clumsy. The Haskell and Ocaml implementations deliberately don't try to be very general in the type inference, and instead try to pick a decidable subset, so the programmer has to add enough type annotations to guide it.
GADTs let you write down basically the same things that you could write as an inductive datatype in a dependent language like Coq and Agda. So (with some patience) you can make a function return a "proof" of anything that can be witnessed by a first-order inductive type, e.g. equations between expressions, list membership, proofs that a term in an object-language is welltyped, etc. The main limitation is that Haskell doesn't have any termination checking, so if you consider it as a dependently typed language there is no way to write a trustworthy proof that uses induction. Also its not very user-friendly, see [2] for some examples.
[1] Basically, GADTs are equivalent to having equations between types. If all the equations are written out in full, it is reasonably straightforward to check whether two types are provably equal. If you want to do type _inference_, i.e. figure out what equality assumptions a given function should make in order to become welltyped, then you run into various undecidable problems (e.g. "rigid E-unification"). My guess would be that if you wrote down a completely general typesystem featuring GADTs, then you would be able to encode arbitrary computations as type-inference problems, but the encoding would be very clumsy. The Haskell and Ocaml implementations deliberately don't try to be very general in the type inference, and instead try to pick a decidable subset, so the programmer has to add enough type annotations to guide it.
[2] https://personal.cis.strath.ac.uk/conor.mcbride/pub/hasochis...