wip

Author: Your Name

src/Hell.hs

@@ -1,3 +1,4 @@
+{-# LANGUAGE DeriveAnyClass #-}
 {-# LANGUAGE AllowAmbiguousTypes #-}
 {-# LANGUAGE BangPatterns #-}
 {-# LANGUAGE BlockArguments #-}
@@ -42,8 +43,13 @@
 
 module Main (main, specMain) where
 
+
 #if __GLASGOW_HASKELL__ >= 906
+import Data.Fix
+import qualified Control.Unification.Types as FD
+import Control.Monad.Except
 import qualified Control.Unification as FD
+import qualified Control.Unification.STVar as FD
 import GHC.Generics (Generic1)
 import Control.Monad
 #endif
@@ -52,6 +58,7 @@ import Control.Monad
 -- e.g. 'Data.Graph' becomes 'Graph', and are then exposed to the Hell
 -- guest language as such.
 
+import Control.Monad.ST
 import qualified Data.CaseInsensitive as CI
 import Data.CaseInsensitive (CI, FoldCase)
 import qualified Network.HTTP.Types as Http
@@ -2646,6 +2653,72 @@ data Ty a
   | TyFun a a
   | TyCon SomeTypeRep
   deriving (Functor, Traversable, Foldable, Eq, Ord, Show, Generic1)
+-- Below: Needed for FD.freeVar (note for myself, not audience)
+deriving instance FD.Unifiable Ty
+
+-- WIP: At this point we want, preferably, a function that goes
+-- from an (IRep IMetaVar) to SomeTypeRep in one go, which inferExp can
+-- use to traverse f iterm to get UTerm SomeTypeRep.
+--
+-- Some key ingredients:
+--
+-- to_sometyperep :: Fix Ty -> Either ZonkError SomeTypeRep
+-- irep_to_uterm :: IRep v -> FD.UTerm Ty v
+-- FD.applyBindings :: UTerm t v -> em m (UTerm t v)
+--
+-- I'd say we want to:
+--
+-- 1) Convert the IRep IMetaVar to UTerm t v using the (Map IMetaVar (STVar ..)) map.
+-- 2) Apply bindings to fully flesh out the type.
+-- 3) Zonk it, going directly from FD.UTerm Ty straight to SomeTypeRep
+--     (tweak to_sometyperep to work with UTerm Ty rather than Fix Ty)
+--
+-- That should be all that's needed?
+
+-- Not useful; leaving for reading purposes.
+st_unstize_var :: FD.STVar s Ty
+               -> FD.STBinding s (Maybe (IRep (FD.STVar s Ty)))
+st_unstize_var stv = do
+  m <- FD.lookupVar stv
+  case m of
+    Nothing -> pure Nothing
+    Just v -> pure $ Just $ uterm_to_irep v
+
+-- Unify all the equality constraints provided.
+st_unifier :: [Equality (FD.UTerm Ty (FD.STVar s Ty))]
+           -> ExceptT (FD.UFailure Ty (FD.STVar s Ty))
+                      (FD.STBinding s)
+                      ()
+st_unifier = traverse_ \(Equality src a b) -> void $ FD.unify a b
+
+-- Run an ST-izing operation, and return the mapping from the original IMetaVars to the STVars, so that they can be recovered later.
+run_stize :: StateT (Map IMetaVar (FD.STVar s Ty)) (FD.STBinding s) x -> FD.STBinding s (x, Map IMetaVar (FD.STVar s Ty))
+run_stize = flip runStateT (mempty :: Map IMetaVar (FD.STVar s Ty))
+
+-- ST-ize the metavars in all types in the equality constraints set
+stize_equalities :: [Equality (IRep IMetaVar)] -> StateT (Map IMetaVar (FD.STVar s Ty)) (FD.STBinding s) [Equality (FD.UTerm Ty (FD.STVar s Ty))]
+stize_equalities = traverse stize_equality
+
+-- ST-ize the metavars in all types in the equality's types on both sides, it also
+-- is exactly where conversion from IRep to UTerm Ty occurs.
+stize_equality :: Equality (IRep IMetaVar) -> StateT (Map IMetaVar (FD.STVar s Ty)) (FD.STBinding s) (Equality (FD.UTerm Ty (FD.STVar s Ty)))
+stize_equality (Equality loc a b) = do
+  Equality loc <$> stize_uterm (irep_to_uterm a) <*> stize_uterm (irep_to_uterm b)
+
+-- ST-ize the metavars in a uterm
+stize_uterm :: FD.UTerm Ty IMetaVar -> StateT (Map IMetaVar (FD.STVar s Ty)) (FD.STBinding s) (FD.UTerm Ty (FD.STVar s Ty))
+stize_uterm = traverse stize_imetavar
+
+-- ST-ize this metavar and remember that it was done
+stize_imetavar :: IMetaVar -> StateT (Map IMetaVar (FD.STVar s Ty)) (FD.STBinding s) (FD.STVar s Ty)
+stize_imetavar = \v -> do
+  mexisting <- gets (Map.lookup v)
+  case mexisting of
+    Just stv -> pure stv
+    Nothing -> do
+      stv <- lift FD.freeVar
+      modify' (Map.insert v stv)
+      pure stv
 
 -- <bijection>
 irep_to_uterm :: IRep v -> FD.UTerm Ty v
@@ -2662,6 +2735,30 @@ uterm_to_irep = \case
   FD.UTerm (TyCon t) -> ICon t
 -- </bijection>
 
+-- | (unification-fd edition)
+-- A complete implementation of conversion from the inferer's type
+-- rep to some star type, ready for the type checker.
+to_sometyperep :: Fix Ty -> Either ZonkError SomeTypeRep
+to_sometyperep t = do
+  go t
+  where
+    go :: Fix Ty -> Either ZonkError SomeTypeRep
+    go = \case
+      Fix (TyCon someTypeRep) -> pure someTypeRep
+      Fix (TyFun a b) -> do
+        a' <- go a
+        b' <- go b
+        case (a', b') of
+          (StarTypeRep aRep, StarTypeRep bRep) ->
+            pure $ StarTypeRep (Type.Fun aRep bRep)
+          _ -> Left ZonkKindError
+      Fix (TyApp f a) -> do
+        f' <- go f
+        a' <- go a
+        case applyTypes f' a' of
+          Just someTypeRep -> pure someTypeRep
+          _ -> Left ZonkKindError
+
 --------------------------------------------------------------------------------
 -- Inference type representation