Re: [Haskell-cafe] Runtime selection on types while capturing a dictionary?

On 8 Oct 2024, at 00:14, Tom Ellis wrote: data PossiblyRootedTree lengths labels where RootedTree :: AugmentedTree [NodeId] lengths labels UnrootedTree :: AugmentedTree () lengths labels

Isn’t that invalid syntax? Wouldn’t you need either data PossiblyRootedTree lengths labels where RootedTree :: AugmentedTree [NodeId] lengths labels -> PossiblyRootedTree lengths labels UnrootedTree :: AugmentedTree () lengths labels -> PossiblyRootedTree lengths labels or simply (avoiding GADT syntax altogether): data PossiblyRootedTree lengths labels = RootedTree (AugmentedTree [NodeId] lengths labels) | UnrootedTree (AugmentedTree () lengths labels)