Algorithmic context well formedness

src/Unison/Type/Context.hs

@@ -5,7 +5,40 @@
 module Unison.Type.Context where
 
 import Unison.Syntax.Type as T
+import Unison.Syntax.Var as V
 import Unison.Type.Context.Element as E
 
 -- | An ordered algorithmic context
 data Context (t :: E.T) sa a v = Context [Element t sa a v]
+
+-- | Extend this `Context` by one element
+extend :: Element t sa a v -> Context t sa a v -> Context t sa a v
+extend e (Context ctx) = Context (e : ctx)
+
+-- | Extend this `Context`
+extendUniversal :: Context t sa a (Var v) -> Context t sa a (Var v)
+extendUniversal (Context ctx) =
+  Context (Universal V.bound1 : map (fmap V.succ) ctx)
+
+universals :: Context t sa a v -> [v]
+universals (Context ctx) = [v | Universal v <- ctx]
+
+existentials :: Context t sa a v -> [v]
+existentials (Context ctx) = ctx >>= go where
+  go (Existential v) = [v]
+  go (Solved v _) = [v]
+  go _ = []
+
+wellformedType :: Eq v => Context t sa a (V.Var v) -> Type t' c k v -> Bool
+wellformedType c t = case t of
+  Unit -> True
+  Var v -> v `elem` universals c
+  Exists v -> v `elem` existentials c
+  Arrow i o -> wellformedType c i && wellformedType c o
+  T.Ann t' _ -> wellformedType c t'
+  Constrain t' _ -> wellformedType c t'
+  -- if there are no deletes in middle, may be more efficient to weaken t'
+  Forall t' -> wellformedType (extendUniversal c) t'
+
+
+

src/Unison/Type/Context/Element.hs

@@ -1,10 +1,15 @@
 {-# LANGUAGE DataKinds #-}
+{-# LANGUAGE DeriveFunctor #-}
+{-# LANGUAGE DeriveFoldable #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE KindSignatures #-}
 {-# LANGUAGE StandaloneDeriving #-}
 
 module Unison.Type.Context.Element where
 
+import Control.Lens
+import Data.Foldable
+
 -- Kind used to tag contexts
 data T = Complete | Incomplete
 
@@ -20,6 +25,39 @@ data Element (t :: T) sa a v where
   Ann :: v -> a -> Element t sa a v             -- | ^ `v` has type `a`, which may be quantified
   Marker :: v -> Element t sa a v               -- | ^ used for scoping somehow
 
+instance Functor (Element t sa a) where
+  fmap f e = case e of
+    Universal v -> Universal (f v)
+    Existential v -> Existential (f v)
+    Solved v sa -> Solved (f v) sa
+    Ann v a -> Ann (f v) a
+    Marker v -> Marker (f v)
+
+_Universal :: Simple Prism (Element t sa a v) v
+_Universal = prism Universal go where
+  go (Universal v) = Right v
+  go e = Left e
+
+_Existential :: Simple Prism (Element Incomplete sa a v) v
+_Existential = prism Existential go where
+  go (Existential v) = Right v
+  go e = Left e
+
+_Solved :: Simple Prism (Element t sa a v) (v, sa)
+_Solved = prism (uncurry Solved) go where
+  go (Solved v t) = Right (v, t)
+  go e = Left e
+
+_Ann :: Simple Prism (Element t sa a v) (v, a)
+_Ann = prism (uncurry Ann) go where
+  go (Ann v t) = Right (v, t)
+  go e = Left e
+
+_Marker :: Simple Prism (Element t sa a v) v
+_Marker = prism Marker go where
+  go (Marker v) = Right v
+  go e = Left e
+
 deriving instance (Eq sa, Eq a, Eq v) => Eq (Element t sa a v)
 deriving instance (Show sa, Show a, Show v) => Show (Element t sa a v)
 deriving instance (Ord sa, Ord a, Ord v) => Ord (Element t sa a v)