Existentials

[ggreif]

This pull request establishes a third way of describing node constructors for gdiff. The new Meta constructor subsumes the functionality of Abstr but is a bit less efficient. The usage recipe is

{-#  LANGUAGE FlexibleContexts, ScopedTypeVariables  #-}

data Hidden = forall t . Type Fam t => Hide t

data Fam ft ts where
  Hidden' :: List Fam ts => Fam t ts -> Fam Hidden ts
  -- ...

instance Family Fam where

instance Type Fam Hidden where
  constructors = [Meta $ \(Hide (a :: t)) -> head $ [ Concr (Hidden' con)
                                                    | Concr con :: Con Fam t <- constructors
                                                    , Just _ <- [fields con a]
                                                    ]
                 ]

With Abstr its is impossible to define a function of type Hidden -> Fam Hidden (Cons a Nil) since it would expose a (skolem constant) unknown existential type. However it is entirely possible to write a function of type Hidden -> Con Fam Hidden as requested by the new Meta way.

[ggreif]

@eelco @kosmikus Any chance to conduct a quick review on these PRs?