From 171bafc69e7bbe2a76427ba7a23d1ede914efc17 Mon Sep 17 00:00:00 2001
From: Rob Rix <robrix@github.com>
Date: Fri, 4 Oct 2019 18:25:47 -0400
Subject: [PATCH] Define Project locally to Data.Core for now.

---
 semantic-core/src/Data/Core.hs | 38 +++++++++++++++++++++++++++++++++-
 1 file changed, 37 insertions(+), 1 deletion(-)

diff --git a/semantic-core/src/Data/Core.hs b/semantic-core/src/Data/Core.hs
index 6691516ae..e50f412f3 100644
--- a/semantic-core/src/Data/Core.hs
+++ b/semantic-core/src/Data/Core.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE DeriveGeneric, DeriveTraversable, FlexibleContexts, LambdaCase, MultiParamTypeClasses, OverloadedStrings, QuantifiedConstraints, RankNTypes,
+{-# LANGUAGE DeriveGeneric, DeriveTraversable, FlexibleContexts, FlexibleInstances, LambdaCase, MultiParamTypeClasses, OverloadedStrings, QuantifiedConstraints, RankNTypes,
              ScopedTypeVariables, StandaloneDeriving, TypeFamilies, TypeOperators, UndecidableInstances #-}
 module Data.Core
 ( Core(..)
@@ -239,3 +239,39 @@ stripAnnotations :: (HFunctor sig, forall g . Functor g => Functor (sig g)) => T
 stripAnnotations (Var v)              = Var v
 stripAnnotations (Term (L (Ann _ b))) = stripAnnotations b
 stripAnnotations (Term (R        b))  = Term (hmap stripAnnotations b)
+
+
+-- | The class of types which can be projected from a signature.
+--
+--   This is based on Wouter Swierstra’s design described in [Data types à la carte](http://www.cs.ru.nl/~W.Swierstra/Publications/DataTypesALaCarte.pdf). As described therein, overlapping instances are required in order to distinguish e.g. left-occurrence from right-recursion.
+--
+--   It should not generally be necessary for you to define new 'Project' instances, but these are not specifically prohibited if you wish to get creative.
+class Project (sub :: (* -> *) -> (* -> *)) sup where
+  -- | Inject a member of a signature into the signature.
+  prj :: sup m a -> Maybe (sub m a)
+
+-- | Reflexivity: @t@ is a member of itself.
+instance Project t t where
+  prj = Just
+
+-- | Left-recursion: if @t@ is a member of @l1 ':+:' l2 ':+:' r@, then we can inject it into @(l1 ':+:' l2) ':+:' r@ by injection into a right-recursive signature, followed by left-association.
+instance {-# OVERLAPPABLE #-}
+         Project t (l1 :+: l2 :+: r)
+      => Project t ((l1 :+: l2) :+: r) where
+  prj = prj . reassoc where
+    reassoc (L (L l)) = L l
+    reassoc (L (R l)) = R (L l)
+    reassoc (R r)     = R (R r)
+
+-- | Left-occurrence: if @t@ is at the head of a signature, we can inject it in O(1).
+instance {-# OVERLAPPABLE #-}
+         Project l (l :+: r) where
+  prj (L l) = Just l
+  prj _     = Nothing
+
+-- | Right-recursion: if @t@ is a member of @r@, we can inject it into @r@ in O(n), followed by lifting that into @l ':+:' r@ in O(1).
+instance {-# OVERLAPPABLE #-}
+         Project l r
+      => Project l (l' :+: r) where
+  prj (R r) = prj r
+  prj _     = Nothing