From 8ea5a67b3de558d8ff3cecf609180bd59a242c96 Mon Sep 17 00:00:00 2001 From: Your Name Date: Sat, 15 Aug 2026 21:07:28 +0100 Subject: [PATCH 1/5] Add unification-fd to package.yaml --- hell.cabal | 2 ++ package.yaml | 1 + 2 files changed, 3 insertions(+) diff --git a/hell.cabal b/hell.cabal index 54c85e3..caa4955 100644 --- a/hell.cabal +++ b/hell.cabal @@ -47,6 +47,7 @@ executable hell , these , time , typed-process + , unification-fd , unliftio , vector , wai @@ -87,6 +88,7 @@ test-suite hell-test , these , time , typed-process + , unification-fd , unliftio , vector , wai diff --git a/package.yaml b/package.yaml index a427634..f2b7752 100644 --- a/package.yaml +++ b/package.yaml @@ -34,6 +34,7 @@ dependencies: - time - warp - wai +- unification-fd - http-types - case-insensitive From 4604cf4dfd3913ea276ff0806c0849a18a77747e Mon Sep 17 00:00:00 2001 From: Your Name Date: Sat, 15 Aug 2026 21:07:42 +0100 Subject: [PATCH 2/5] Add basic bijection to/from FD.UTerm --- src/Hell.hs | 28 +++++++++++++++++++++++++++- 1 file changed, 27 insertions(+), 1 deletion(-) diff --git a/src/Hell.hs b/src/Hell.hs index 9bfdcf5..2544391 100644 --- a/src/Hell.hs +++ b/src/Hell.hs @@ -3,7 +3,7 @@ {-# LANGUAGE BlockArguments #-} {-# LANGUAGE CPP #-} {-# LANGUAGE DataKinds #-} -{-# LANGUAGE DeriveFoldable #-} +{-# LANGUAGE DeriveFoldable, DeriveGeneric #-} {-# LANGUAGE DeriveFunctor #-} {-# LANGUAGE DeriveTraversable #-} {-# LANGUAGE ExistentialQuantification, DuplicateRecordFields, NoFieldSelectors #-} @@ -43,6 +43,8 @@ module Main (main, specMain) where #if __GLASGOW_HASKELL__ >= 906 +import qualified Control.Unification as FD +import GHC.Generics (Generic1) import Control.Monad #endif @@ -2636,6 +2638,30 @@ temp_withSystemTempDirectory template action = Temp.withSystemTempDirectory (Tex process_setWorkingDir :: forall a b c. Text -> ProcessConfig a b c -> ProcessConfig a b c process_setWorkingDir filepath = Process.setWorkingDir (Text.unpack filepath) +-------------------------------------------------------------------------------- +-- unification-fd compatibility layer + +data Ty a + = TyApp a a + | TyFun a a + | TyCon SomeTypeRep + deriving (Functor, Traversable, Foldable, Eq, Ord, Show, Generic1) + +-- +irep_to_uterm :: IRep v -> FD.UTerm Ty v +irep_to_uterm = \case + IVar v -> FD.UVar v + IApp f x -> FD.UTerm (TyApp (irep_to_uterm f) (irep_to_uterm x)) + IFun f x -> FD.UTerm (TyFun (irep_to_uterm f) (irep_to_uterm x)) + ICon t -> FD.UTerm $ TyCon t +uterm_to_irep :: FD.UTerm Ty v -> IRep v +uterm_to_irep = \case + FD.UVar v -> IVar v + FD.UTerm (TyApp f x) -> IApp (uterm_to_irep f) (uterm_to_irep x) + FD.UTerm (TyFun f x) -> IFun (uterm_to_irep f) (uterm_to_irep x) + FD.UTerm (TyCon t) -> ICon t +-- + -------------------------------------------------------------------------------- -- Inference type representation From 1bc6ea3f0a681075098668e21b6ceb9b64315fd9 Mon Sep 17 00:00:00 2001 From: Your Name Date: Sat, 15 Aug 2026 21:33:07 +0100 Subject: [PATCH 3/5] unification-fd based unifier: MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit chris@linux:~/Work/chrisdone/hell$ ./hell-status-quo --check /home/chris/Work/artificialio/brossa-infra/.github/workflows/scripts/summarise.hell --compiler-stats stat: read_file = 68.75 μs stat: parse_module_with_mode = 16.34 ms stat: resolve_module = 72.12 μs stat: parse = 16.60 ms stat: cycle_detect = 65.45 ms stat: desugar = 54.18 ms stat: elaborate = 1.590 ms stat: unify = 638.1 ms stat: zonk = 688.6 ms stat: infer = 1.328 s stat: check = 2.804 ms chris@linux:~/Work/chrisdone/hell$ ./hell-ufd --check /home/chris/Work/artificialio/brossa-infra/.github/workflows/scripts/summarise.hell --compiler-stats stat: read_file = 114.2 μs stat: parse_module_with_mode = 29.61 ms stat: resolve_module = 79.21 μs stat: parse = 30.09 ms stat: cycle_detect = 63.70 ms stat: desugar = 62.56 ms stat: elaborate = 3.719 ms stat: unify-and-zonk = 270.5 ms stat: infer = 274.4 ms stat: check = 2.561 ms --- hell.cabal | 4 ++ package.yaml | 2 + src/Hell.hs | 165 ++++++++++++++++++++++++++++++++++++++++++++++++--- 3 files changed, 163 insertions(+), 8 deletions(-) diff --git a/hell.cabal b/hell.cabal index caa4955..cc980a7 100644 --- a/hell.cabal +++ b/hell.cabal @@ -30,6 +30,7 @@ executable hell , containers , criterion , criterion-measurement + , data-fix , directory , ghc-prim , haskell-src-exts @@ -46,6 +47,7 @@ executable hell , th-orphans , these , time + , transformers , typed-process , unification-fd , unliftio @@ -71,6 +73,7 @@ test-suite hell-test , containers , criterion , criterion-measurement + , data-fix , directory , ghc-prim , haskell-src-exts @@ -87,6 +90,7 @@ test-suite hell-test , th-orphans , these , time + , transformers , typed-process , unification-fd , unliftio diff --git a/package.yaml b/package.yaml index f2b7752..5ffb2d7 100644 --- a/package.yaml +++ b/package.yaml @@ -35,6 +35,8 @@ dependencies: - warp - wai - unification-fd +- transformers +- data-fix - http-types - case-insensitive diff --git a/src/Hell.hs b/src/Hell.hs index 2544391..c492f2a 100644 --- a/src/Hell.hs +++ b/src/Hell.hs @@ -1,3 +1,4 @@ +{-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE BangPatterns #-} {-# LANGUAGE BlockArguments #-} @@ -42,8 +43,14 @@ module Main (main, specMain) where + #if __GLASGOW_HASKELL__ >= 906 +import Data.Tuple +import Data.Fix +import qualified Control.Unification.Types as FD +import Control.Monad.Trans.Except import qualified Control.Unification as FD +import qualified Control.Unification.STVar as FD import GHC.Generics (Generic1) import Control.Monad #endif @@ -52,6 +59,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 @@ -211,7 +219,7 @@ compileFile stats filePath = do case lookup "main" dterms of Nothing -> error "No main declaration!" Just main' -> do - inferred <- inferExp (nestStat stats) main' + inferred <- infer_exp (nestStat stats) main' case inferred of Left err -> error $ prettyString err Right uterm -> do @@ -1636,7 +1644,10 @@ data InferError = UnifyError UnifyError | ZonkError ZonkError | ElabError ElaborateError - deriving (Show) + | ST_mapping_error + | ST_unify_error + | ST_apply_bindings_error +deriving instance Show InferError -- | Note: All types in the input are free of metavars. There is an -- intermediate phase in which there are metavars, but then they're @@ -1665,6 +1676,19 @@ inferExp stats uterm = do emitStat stats "zonk" (t3 - t2) pure $ Right sterm +infer_exp :: + StatsEnabled -> + UTerm () -> + IO (Either InferError (UTerm SomeTypeRep)) +infer_exp stats uterm = do + t0 <- getTime + case elaborate uterm of + Left elabError -> pure $ Left $ ElabError elabError + Right (iterm, equalities) -> do + t1 <- getTime + emitStat stats "elaborate" (t1 - t0) + st_unify stats equalities iterm + -- | Zonk a type and then convert it to a type: t :: * zonkToStarType :: Map IMetaVar (IRep IMetaVar) -> IRep IMetaVar -> Either ZonkError SomeTypeRep zonkToStarType subs irep = do @@ -2646,6 +2670,103 @@ 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. Or it receives the expr +-- to traverse over, due to the ST monadness. +-- +-- 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? + +-- Unify all the constraints in @equalities@, zonk and update the term and return it. +st_unify :: Traversable t + => StatsEnabled + -> Set (Equality (IRep IMetaVar)) + -> t (IRep IMetaVar) + -> IO (Either InferError (t SomeTypeRep)) +st_unify stats set term = do + t1 <- getTime + let result = + FD.runSTBinding do + -- Thaw the equalities. + (equalities, mapping) <- run_stize $ stize_equalities $ Set.toList set + -- Unify the mutable equalities into the ambient environment. + result <- runExceptT $ st_unifier_ equalities + case result of + Left err -> pure $ Left ST_unify_error + Right () -> do + -- Apply bindings, zonk and freeze all the types across the term. + runExceptT $ + for term \irepmv -> do + uterm <- for (irep_to_uterm irepmv) \imv -> + case Map.lookup imv mapping of + Nothing -> throwE $ ST_mapping_error + Just stvar -> pure stvar + uterm' <- withExceptT (const ST_apply_bindings_error) $ st_apply uterm + except $ first ZonkError $ + to_sometyperep + mapping + uterm' + case result of + Left err -> pure $ Left err + Right (!term') -> do + t2 <- getTime + emitStat stats "unify-and-zonk" (t2 - t1) + pure $ Right term' + +-- Apply bindings; this type signature avoids type inference problems. +st_apply :: FD.UTerm Ty (FD.STVar s Ty) + -> ExceptT (FD.UFailure Ty (FD.STVar s Ty)) (FD.STBinding s) (FD.UTerm Ty (FD.STVar s Ty)) +st_apply = FD.applyBindings + +-- 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 -- irep_to_uterm :: IRep v -> FD.UTerm Ty v @@ -2654,14 +2775,36 @@ irep_to_uterm = \case IApp f x -> FD.UTerm (TyApp (irep_to_uterm f) (irep_to_uterm x)) IFun f x -> FD.UTerm (TyFun (irep_to_uterm f) (irep_to_uterm x)) ICon t -> FD.UTerm $ TyCon t -uterm_to_irep :: FD.UTerm Ty v -> IRep v -uterm_to_irep = \case - FD.UVar v -> IVar v - FD.UTerm (TyApp f x) -> IApp (uterm_to_irep f) (uterm_to_irep x) - FD.UTerm (TyFun f x) -> IFun (uterm_to_irep f) (uterm_to_irep x) - FD.UTerm (TyCon t) -> ICon t -- +-- | (unification-fd edition) +-- A complete implementation of conversion from the inferer's type +-- rep to some star type, ready for the type checker. +-- Jumps straight from UTerm Ty to SomeTypeRep in one go; handles +-- ambiguous vars and kind errors here. +to_sometyperep :: forall v. Eq v => (Map IMetaVar v) -> + FD.UTerm Ty v -> Either ZonkError SomeTypeRep +to_sometyperep mapping t = do + go t + where + go :: FD.UTerm Ty v -> Either ZonkError SomeTypeRep + go = \case + FD.UVar k -> Left $ ST_ambiguous_var (List.lookup k $ map swap $ Map.toList mapping) + FD.UTerm (TyCon someTypeRep) -> pure someTypeRep + FD.UTerm (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 + FD.UTerm (TyApp f a) -> do + f' <- go f + a' <- go a + case applyTypes f' a' of + Just someTypeRep -> pure someTypeRep + _ -> Left ZonkKindError + -------------------------------------------------------------------------------- -- Inference type representation @@ -2675,6 +2818,7 @@ data IRep v data ZonkError = ZonkKindError | AmbiguousMetavar IMetaVar + | ST_ambiguous_var (Maybe IMetaVar) deriving (Show) -- | A complete implementation of conversion from the inferer's type @@ -3109,6 +3253,11 @@ instance (Pretty a) => Pretty (IRep a) where instance Pretty ZonkError where pretty = \case ZonkKindError -> "Kind error." + ST_ambiguous_var imetavar -> "(ST) Ambiguous meta variable: " + <> maybe "???" pretty imetavar + <> "\n" + <> "arising from " + <> maybe "???" (pretty . (.srcSpanInfo)) imetavar AmbiguousMetavar imetavar -> "Ambiguous meta variable: " <> pretty imetavar From 23c35e559f25493c132f9c24d0940642073c5928 Mon Sep 17 00:00:00 2001 From: Your Name Date: Mon, 17 Aug 2026 17:28:34 +0100 Subject: [PATCH 4/5] Cleanup warnings --- src/Hell.hs | 162 ++++------------------------------------------------ 1 file changed, 11 insertions(+), 151 deletions(-) diff --git a/src/Hell.hs b/src/Hell.hs index c492f2a..a83ec4c 100644 --- a/src/Hell.hs +++ b/src/Hell.hs @@ -45,21 +45,20 @@ module Main (main, specMain) where #if __GLASGOW_HASKELL__ >= 906 +import Control.Monad +#endif + import Data.Tuple -import Data.Fix import qualified Control.Unification.Types as FD import Control.Monad.Trans.Except import qualified Control.Unification as FD import qualified Control.Unification.STVar as FD import GHC.Generics (Generic1) -import Control.Monad -#endif -- All modules tend to be imported qualified by their last component, -- 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 @@ -113,7 +112,6 @@ import Data.Tree (Tree) import qualified Data.Tree as Tree import Data.Vector (Vector) import qualified Data.Vector as Vector -import Data.Void import GHC.TypeLits import GHC.Types (Type) import qualified Language.Haskell.Exts as HSE @@ -1641,8 +1639,7 @@ desugarAll types0 terms0 = do -- Infer data InferError - = UnifyError UnifyError - | ZonkError ZonkError + = ZonkError ZonkError | ElabError ElaborateError | ST_mapping_error | ST_unify_error @@ -1653,29 +1650,6 @@ deriving instance Show InferError -- intermediate phase in which there are metavars, but then they're -- all eliminated. By the type system, the output contains only -- determinate types. -inferExp :: - StatsEnabled -> - UTerm () -> - IO (Either InferError (UTerm SomeTypeRep)) -inferExp stats uterm = do - t0 <- getTime - case elaborate uterm of - Left elabError -> pure $ Left $ ElabError elabError - Right (iterm, equalities) -> do - t1 <- getTime - emitStat stats "elaborate" (t1 - t0) - case unify equalities of - Left unifyError -> pure $ Left $ UnifyError unifyError - Right subs -> do - t2 <- getTime - emitStat stats "unify" (t2 - t1) - case traverse (zonkToStarType subs) iterm of - Left zonkError -> pure $ Left $ ZonkError $ zonkError - Right !sterm -> do - t3 <- getTime - emitStat stats "zonk" (t3 - t2) - pure $ Right sterm - infer_exp :: StatsEnabled -> UTerm () -> @@ -1689,12 +1663,6 @@ infer_exp stats uterm = do emitStat stats "elaborate" (t1 - t0) st_unify stats equalities iterm --- | Zonk a type and then convert it to a type: t :: * -zonkToStarType :: Map IMetaVar (IRep IMetaVar) -> IRep IMetaVar -> Either ZonkError SomeTypeRep -zonkToStarType subs irep = do - zonked <- zonk (substitute subs irep) - toSomeTypeRep zonked - -------------------------------------------------------------------------------- -- Occurs check @@ -2706,9 +2674,9 @@ st_unify stats set term = do -- Thaw the equalities. (equalities, mapping) <- run_stize $ stize_equalities $ Set.toList set -- Unify the mutable equalities into the ambient environment. - result <- runExceptT $ st_unifier_ equalities - case result of - Left err -> pure $ Left ST_unify_error + result' <- runExceptT $ st_unifier_ equalities + case result' of + Left _err -> pure $ Left ST_unify_error Right () -> do -- Apply bindings, zonk and freeze all the types across the term. runExceptT $ @@ -2737,7 +2705,7 @@ st_apply = FD.applyBindings -- 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 +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)) @@ -2821,30 +2789,6 @@ data ZonkError | ST_ambiguous_var (Maybe IMetaVar) deriving (Show) --- | A complete implementation of conversion from the inferer's type --- rep to some star type, ready for the type checker. -toSomeTypeRep :: IRep Void -> Either ZonkError SomeTypeRep -toSomeTypeRep t = do - go t - where - go :: IRep Void -> Either ZonkError SomeTypeRep - go = \case - IVar v -> pure (absurd v) - ICon someTypeRep -> pure someTypeRep - IFun 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 - IApp f a -> do - f' <- go f - a' <- go a - case applyTypes f' a' of - Just someTypeRep -> pure someTypeRep - _ -> Left ZonkKindError - -- | Convert from a type-indexed type to an untyped type. fromSomeStarType :: forall void. SomeStarType -> IRep void fromSomeStarType (SomeStarType r) = fromSomeType (SomeTypeRep r) @@ -2961,78 +2905,6 @@ freshIMetaVar srcSpanInfo = do modify \elaborate' -> elaborate' {counter = counter + 1} pure $ IMetaVar0 counter srcSpanInfo --------------------------------------------------------------------------------- --- Unification - -data UnifyError - = OccursCheck - | TypeMismatch HSE.SrcSpanInfo (IRep IMetaVar) (IRep IMetaVar) - deriving (Show) - --- | Unification of equality constraints, a ~ b, to substitutions. -unify :: Set (Equality (IRep IMetaVar)) -> Either UnifyError (Map IMetaVar (IRep IMetaVar)) -unify = foldM update mempty - where - update existing equality = - fmap - (`extends` existing) - (examine (fmap (substitute existing) equality)) - examine (Equality l a b) - | a == b = pure mempty - | IVar ivar <- a = bindMetaVar ivar b - | IVar ivar <- b = bindMetaVar ivar a - | IFun a1 b1 <- a, - IFun a2 b2 <- b = - unify (Set.fromList [Equality l a1 a2, Equality l b1 b2]) - | IApp a1 b1 <- a, - IApp a2 b2 <- b = - unify (Set.fromList [Equality l a1 a2, Equality l b1 b2]) - | ICon x <- a, - ICon y <- b = - if x == y - then pure mempty - else Left $ TypeMismatch l a b - | otherwise = Left $ TypeMismatch l a b - --- | Apply new substitutions to the old ones, and expand the set to old+new. -extends :: Map IMetaVar (IRep IMetaVar) -> Map IMetaVar (IRep IMetaVar) -> Map IMetaVar (IRep IMetaVar) -extends new old = fmap (substitute new) old <> new - --- | Apply any substitutions to the type, where there are metavars. -substitute :: Map IMetaVar (IRep IMetaVar) -> IRep IMetaVar -> IRep IMetaVar -substitute subs = go - where - go = \case - IVar v -> case Map.lookup v subs of - Nothing -> IVar v - Just ty -> ty - ICon c -> ICon c - IFun a b -> IFun (go a) (go b) - IApp a b -> IApp (go a) (go b) - --- | Do an occurrs check, if all good, return a binding. -bindMetaVar :: - IMetaVar -> - IRep IMetaVar -> - Either UnifyError (Map IMetaVar (IRep IMetaVar)) -bindMetaVar var typ - | occurs var typ = Left OccursCheck - | otherwise = pure $ Map.singleton var typ - --- | Occurs check. -occurs :: IMetaVar -> IRep IMetaVar -> Bool -occurs ivar = any (== ivar) - --- | Remove any metavars from the type. --- --- -zonk :: IRep IMetaVar -> Either ZonkError (IRep Void) -zonk = \case - IVar var -> Left $ AmbiguousMetavar var - ICon c -> pure $ ICon c - IFun a b -> IFun <$> zonk a <*> zonk b - IApp a b -> IApp <$> zonk a <*> zonk b - -------------------------------------------------------------------------------- -- Parse with #!/shebangs @@ -3271,20 +3143,6 @@ instance Pretty ElaborateError where BadInstantiationBug -> "BUG: BadInstantiationBug. Please report." VariableNotInScope s -> "Variable not in scope: " <> pretty s -instance Pretty UnifyError where - pretty = \case - OccursCheck -> "Occurs check failed: Infinite type." - TypeMismatch l a b -> - mconcat $ - List.intersperse - "\n\n" - [ "Couldn't match type", - " " <> pretty a, - "against type", - " " <> pretty b, - "arising from " <> pretty l - ] - instance Pretty HSE.SrcSpanInfo where pretty l = mconcat @@ -3330,9 +3188,11 @@ instance Pretty DesugarError where instance Pretty InferError where pretty = \case - UnifyError e -> "Unification error: " <> pretty e ZonkError e -> "Zonk error: " <> pretty e ElabError e -> "Elaboration error: " <> pretty e + ST_mapping_error -> "BUG: Unification meta mapping error." + ST_unify_error -> "Unification error!" + ST_apply_bindings_error -> "Unification apply bindings error." -------------------------------------------------------------------------------- -- Generate docs From 87038636ef5ae6b3577a13ce903a01c5afe0200d Mon Sep 17 00:00:00 2001 From: Your Name Date: Mon, 17 Aug 2026 17:30:16 +0100 Subject: [PATCH 5/5] Drop old commentary --- src/Hell.hs | 22 ---------------------- 1 file changed, 22 deletions(-) diff --git a/src/Hell.hs b/src/Hell.hs index a83ec4c..36aa46f 100644 --- a/src/Hell.hs +++ b/src/Hell.hs @@ -2641,26 +2641,6 @@ data Ty a -- 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. Or it receives the expr --- to traverse over, due to the ST monadness. --- --- 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? - -- Unify all the constraints in @equalities@, zonk and update the term and return it. st_unify :: Traversable t => StatsEnabled @@ -2736,14 +2716,12 @@ stize_imetavar = \v -> do modify' (Map.insert v stv) pure stv --- irep_to_uterm :: IRep v -> FD.UTerm Ty v irep_to_uterm = \case IVar v -> FD.UVar v IApp f x -> FD.UTerm (TyApp (irep_to_uterm f) (irep_to_uterm x)) IFun f x -> FD.UTerm (TyFun (irep_to_uterm f) (irep_to_uterm x)) ICon t -> FD.UTerm $ TyCon t --- -- | (unification-fd edition) -- A complete implementation of conversion from the inferer's type