hypertypes 0.1.0.2 → 0.2.2

raw patch · 103 files changed

+4492/−3737 lines, 103 filesdep +tastydep +tasty-hunitdep −QuickChecksetup-changedPVP ok

version bump matches the API change (PVP)

Dependencies added: tasty, tasty-hunit

Dependencies removed: QuickCheck

API changes (from Hackage documentation)

Files

• README.md +5/−7
• Setup.hs +1/−0
• hypertypes.cabal +30/−25
• src/Hyper.hs +15/−16
• src/Hyper/Class/Apply.hs +3/−3
• src/Hyper/Class/Context.hs +62/−58
• src/Hyper/Class/Foldable.hs +14/−11
• src/Hyper/Class/Functor.hs +9/−9
• src/Hyper/Class/HasPlain.hs +4/−4
• src/Hyper/Class/Infer.hs +27/−24
• src/Hyper/Class/Infer/Env.hs +1/−2
• src/Hyper/Class/Infer/InferOf.hs +9/−26
• src/Hyper/Class/Monad.hs +11/−10
• src/Hyper/Class/Morph.hs +13/−7
• src/Hyper/Class/Nodes.hs +24/−11
• src/Hyper/Class/Optic.hs +3/−2
• src/Hyper/Class/Pointed.hs +3/−4
• src/Hyper/Class/Recursive.hs +23/−21
• src/Hyper/Class/Traversable.hs +13/−11
• src/Hyper/Class/Unify.hs +74/−69
• src/Hyper/Class/ZipMatch.hs +25/−15
• src/Hyper/Combinator/ANode.hs +13/−9
• src/Hyper/Combinator/Ann.hs +57/−39
• src/Hyper/Combinator/Compose.hs +107/−76
• src/Hyper/Combinator/Flip.hs +19/−17
• src/Hyper/Combinator/Func.hs +4/−2
• src/Hyper/Diff.hs +77/−55
• src/Hyper/Infer.hs +27/−27
• src/Hyper/Infer/Blame.hs +44/−41
• src/Hyper/Infer/Result.hs +12/−6
• src/Hyper/Infer/ScopeLevel.hs +8/−6
• src/Hyper/Internal/Prelude.hs +10/−11
• src/Hyper/Recurse.hs +54/−37
• src/Hyper/Syntax.hs +12/−0
• src/Hyper/Syntax/App.hs +72/−0
• src/Hyper/Syntax/FuncType.hs +45/−0
• src/Hyper/Syntax/Lam.hs +76/−0
• src/Hyper/Syntax/Let.hs +80/−0
• src/Hyper/Syntax/Map.hs +45/−0
• src/Hyper/Syntax/Nominal.hs +398/−0
• src/Hyper/Syntax/Row.hs +184/−0
• src/Hyper/Syntax/Scheme.hs +279/−0
• src/Hyper/Syntax/Scheme/AlphaEq.hs +119/−0
• src/Hyper/Syntax/TypeSig.hs +69/−0
• src/Hyper/Syntax/TypedLam.hs +82/−0
• src/Hyper/Syntax/Var.hs +70/−0
• src/Hyper/TH/Apply.hs +30/−24
• src/Hyper/TH/Context.hs +34/−24
• src/Hyper/TH/Foldable.hs +30/−25
• src/Hyper/TH/Functor.hs +25/−21
• src/Hyper/TH/HasPlain.hs +82/−79
• src/Hyper/TH/Internal/Utils.hs +128/−104
• src/Hyper/TH/Morph.hs +63/−47
• src/Hyper/TH/Nodes.hs +30/−19
• src/Hyper/TH/Pointed.hs +15/−14
• src/Hyper/TH/Traversable.hs +36/−30
• src/Hyper/TH/ZipMatch.hs +22/−23
• src/Hyper/Type.hs +4/−3
• src/Hyper/Type/AST/App.hs +0/−64
• src/Hyper/Type/AST/FuncType.hs +0/−38
• src/Hyper/Type/AST/Lam.hs +0/−67
• src/Hyper/Type/AST/Let.hs +0/−68
• src/Hyper/Type/AST/Map.hs +0/−40
• src/Hyper/Type/AST/Nominal.hs +0/−361
• src/Hyper/Type/AST/Row.hs +0/−163
• src/Hyper/Type/AST/Scheme.hs +0/−268
• src/Hyper/Type/AST/Scheme/AlphaEq.hs +0/−112
• src/Hyper/Type/AST/TypeSig.hs +0/−61
• src/Hyper/Type/AST/TypedLam.hs +0/−69
• src/Hyper/Type/AST/Var.hs +0/−64
• src/Hyper/Type/Functor.hs +21/−12
• src/Hyper/Type/Prune.hs +42/−25
• src/Hyper/Type/Pure.hs +9/−5
• src/Hyper/Unify.hs +40/−35
• src/Hyper/Unify/Binding.hs +28/−25
• src/Hyper/Unify/Binding/ST.hs +13/−12
• src/Hyper/Unify/Binding/ST/Load.hs +48/−38
• src/Hyper/Unify/Binding/Save.hs +34/−34
• src/Hyper/Unify/Constraints.hs +13/−10
• src/Hyper/Unify/Error.hs +31/−28
• src/Hyper/Unify/Generalize.hs +118/−104
• src/Hyper/Unify/New.hs +7/−4
• src/Hyper/Unify/Occurs.hs +28/−28
• src/Hyper/Unify/QuantifiedVar.hs +9/−6
• src/Hyper/Unify/Term.hs +34/−25
• test/AlphaEqTest.hs +103/−0
• test/Benchmark.hs +3/−1
• test/BlameTest.hs +59/−0
• test/ExprUtils.hs +101/−0
• test/Hyper/Class/Infer/Infer1.hs +5/−3
• test/Hyper/Syntax/NamelessScope.hs +134/−0
• test/Hyper/Syntax/NamelessScope/InvDeBruijn.hs +39/−0
• test/Hyper/Type/AST/NamelessScope.hs +0/−128
• test/Hyper/Type/AST/NamelessScope/InvDeBruijn.hs +0/−34
• test/LangA.hs +84/−68
• test/LangATest.hs +85/−0
• test/LangB.hs +104/−80
• test/LangBTest.hs +297/−0
• test/LangC.hs +57/−52
• test/LangD.hs +10/−1
• test/ReadMeExamples.hs +24/−13
• test/Spec.hs +14/−459
• test/TypeLang.hs +67/−58

@@ -6,7 +6,7 @@  > The goal is to define a data type by cases, where one can add new cases to the data type and new functions over the data type, without recompiling existing code, and while retaining static type safety. -[*Data types a la carte*](http://www.cs.ru.nl/~W.Swierstra/Publications/DataTypesALaCarte.pdf) (DTALC, Swierstra, 2008) offers a solution for the expression problem which is only applicable for simple recursive expressions, without support for mutually recursive types. In practice, programming language ASTs do tend to be mutually recursive. [`multirec`](http://hackage.haskell.org/package/multirec) (Rodriguez et al, 2009) uses GADTs to encode mutually recursive types but in comparison to DTALC it lacks in the ability to construct the types from re-usable components.+[*Data types a la carte*](http://www.staff.science.uu.nl/~swier004/publications/2008-jfp.pdf) (DTALC, Swierstra, 2008) offers a solution for the expression problem which is only applicable for simple recursive expressions, without support for mutually recursive types. In practice, programming language ASTs do tend to be mutually recursive. [`multirec`](http://hackage.haskell.org/package/multirec) (Rodriguez et al, 2009) uses GADTs to encode mutually recursive types but in comparison to DTALC it lacks in the ability to construct the types from re-usable components.  Hypertypes allow constructing expressions from re-usable terms like DTALC, which can be rich mutually recursive types like in `multirec`. @@ -246,7 +246,7 @@  The `hypertypes` library provides: -* Variants of standard classes like `Functor` with `TemplateHaskell` derivations for hypertypes.+* Variants of standard classes like `Functor` for hypertypes with derivations.   (Unlike in `multirec`'s `HFunctor`, only the actual child node types of each node need to be handled) * Combinators for recursive processing and transformation of nested structures * Implementations of common AST terms@@ -289,7 +289,7 @@ To write it more consicely, the `HasHPlain` class, along with a `TemplateHaskell` generator for it, exists:  ```Haskell-> let e = hPlain :# verboseExpr+> let e = hPlain # verboseExpr -- Note: This (#) comes from Control.Lens  > e@@ -434,8 +434,6 @@  * `DerivingStrategies`, `LambdaCase`, `TupleSections`, `TypeOperators` -Some extensions we use but would like to avoid (we're looking for alternative solutions but haven't found them):- ## How does hypertypes compare/relate to  Note that comparisons to `multirec`, HKD, `recursion-schemes`, `rank2classes`, and `unification-fd` were discussed above.@@ -502,9 +500,9 @@  Unlike a DTALC-based apply, which would be parameterized by a single type parameter `(a :: Type)`, `App` is parameterized on two type parameters, `(expr :: HyperType)` and `(h :: AHyperType)`. `expr` represents the node type of `App expr`'s child nodes and `h` is the tree's fix-point. This enables using `App` in mutually recursive ASTs where it may be parameterized by several different `expr`s. -Unlike the original DTALC paper which isn't suitable for mutually recursive ASTs, in `hypertypes` one would have to declare an explicit expression type for each expression type for use as `App`'s `expr` type parameter. Similarly, `multirec`'s DTALC variant also requires explicitly declaring type indices.+Unlike DTALC, in `hypertypes` one typically needs to explicitly declare the datatypes for their expression types so that they can be used as `App`'s `expr` type parameter. Similarly, `multirec`'s DTALC variant also requires explicitly declaring type indices. -While it is possible to declare ASTs as `newtype`s wrapping `:+:`s of existing terms and deriving all the instances via `GeneralizedNewtypeDeriving`, our usage and examples declare types in the straight forward way, with named data constructors, as we think results in more readable and performant code.+While it is possible to declare ASTs as `newtype`s wrapping `:+:`s of existing terms and deriving all the instances via `GeneralizedNewtypeDeriving`, our usage and examples declare types in the straight forward way, with named data constructors, as we think that this results in more readable and performant code.  ### bound 

@@ -1,2 +1,3 @@ import Distribution.Simple+ main = defaultMain

@@ -1,13 +1,11 @@ cabal-version: 1.12 --- This file has been generated from package.yaml by hpack version 0.34.4.+-- This file has been generated from package.yaml by hpack version 0.35.2. -- -- see: https://github.com/sol/hpack------ hash: 2cd28816c22eeee72d7eaf5cbf22e66156807737fd967437f6ccdd5108df3649  name:           hypertypes-version:        0.1.0.2+version:        0.2.2 synopsis:       Typed ASTs description:    Please see the README on GitHub at <https://github.com/lamdu/hypertypes#readme> category:       Algorithms, Compilers/Interpreters, Language, Logic, Unification@@ -58,6 +56,19 @@       Hyper.Infer.Result       Hyper.Infer.ScopeLevel       Hyper.Recurse+      Hyper.Syntax+      Hyper.Syntax.App+      Hyper.Syntax.FuncType+      Hyper.Syntax.Lam+      Hyper.Syntax.Let+      Hyper.Syntax.Map+      Hyper.Syntax.Nominal+      Hyper.Syntax.Row+      Hyper.Syntax.Scheme+      Hyper.Syntax.Scheme.AlphaEq+      Hyper.Syntax.TypedLam+      Hyper.Syntax.TypeSig+      Hyper.Syntax.Var       Hyper.TH.Apply       Hyper.TH.Context       Hyper.TH.Foldable@@ -69,18 +80,6 @@       Hyper.TH.Traversable       Hyper.TH.ZipMatch       Hyper.Type-      Hyper.Type.AST.App-      Hyper.Type.AST.FuncType-      Hyper.Type.AST.Lam-      Hyper.Type.AST.Let-      Hyper.Type.AST.Map-      Hyper.Type.AST.Nominal-      Hyper.Type.AST.Row-      Hyper.Type.AST.Scheme-      Hyper.Type.AST.Scheme.AlphaEq-      Hyper.Type.AST.TypedLam-      Hyper.Type.AST.TypeSig-      Hyper.Type.AST.Var       Hyper.Type.Functor       Hyper.Type.Prune       Hyper.Type.Pure@@ -119,11 +118,10 @@       TypeOperators       TypeFamilies       NoImplicitPrelude-  ghc-options: -fexpose-all-unfoldings -Wall -Wcompat -Wredundant-constraints -Wnoncanonical-monad-instances -Wincomplete-record-updates -Wincomplete-uni-patterns+  ghc-options: -fexpose-all-unfoldings -Wall -Wcompat -Wredundant-constraints -Wunused-packages -Wnoncanonical-monad-instances -Wincomplete-record-updates -Wincomplete-uni-patterns   ghc-prof-options: -fexpose-all-unfoldings   build-depends:-      QuickCheck-    , array+      array     , base >=4.9 && <5     , base-compat     , binary@@ -147,11 +145,16 @@   type: exitcode-stdio-1.0   main-is: Spec.hs   other-modules:+      AlphaEqTest+      BlameTest+      ExprUtils       Hyper.Class.Infer.Infer1-      Hyper.Type.AST.NamelessScope-      Hyper.Type.AST.NamelessScope.InvDeBruijn+      Hyper.Syntax.NamelessScope+      Hyper.Syntax.NamelessScope.InvDeBruijn       LangA+      LangATest       LangB+      LangBTest       LangC       LangD       ReadMeExamples@@ -176,7 +179,8 @@       TypeApplications       TypeOperators       TypeFamilies-  ghc-options: -fexpose-all-unfoldings -Wall -Wcompat -Wredundant-constraints -threaded -rtsopts -with-rtsopts=-N+      NoImplicitPrelude+  ghc-options: -fexpose-all-unfoldings -Wall -Wcompat -Wredundant-constraints -Wunused-packages -threaded -rtsopts -with-rtsopts=-N   ghc-prof-options: -fexpose-all-unfoldings   build-depends:       base >=4.9 && <5@@ -190,8 +194,9 @@     , monad-st     , mtl     , pretty+    , tasty+    , tasty-hunit     , text-    , transformers   default-language: Haskell2010  benchmark hypertypes-bench@@ -219,7 +224,8 @@       TypeApplications       TypeOperators       TypeFamilies-  ghc-options: -fexpose-all-unfoldings -Wall -Wcompat -Wredundant-constraints -O2 -Wnoncanonical-monad-instances -Wincomplete-record-updates -Wincomplete-uni-patterns+      NoImplicitPrelude+  ghc-options: -fexpose-all-unfoldings -Wall -Wcompat -Wredundant-constraints -Wunused-packages -O2 -Wnoncanonical-monad-instances -Wincomplete-record-updates -Wincomplete-uni-patterns   ghc-prof-options: -fexpose-all-unfoldings   build-depends:       base >=4.9 && <5@@ -234,5 +240,4 @@     , monad-st     , mtl     , pretty-    , transformers   default-language: Haskell2010

@@ -1,29 +1,28 @@ -- | A convinience module which re-exports common functionality of the hypertypes library- module Hyper (module X) where -import Data.Constraint as X (Constraint, Dict(..), withDict)-import Data.Functor.Const as X (Const(..))-import Data.Proxy as X (Proxy(..))-import GHC.Generics as X (Generic, (:*:)(..))-import Hyper.Class.Apply as X (HApply(..), HApplicative, liftH2)-import Hyper.Class.Foldable as X (HFoldable(..), hfoldMap, hfolded1, htraverse_, htraverse1_)-import Hyper.Class.Functor as X (HFunctor(..), hmapped1)-import Hyper.Class.HasPlain as X (HasHPlain(..))-import Hyper.Class.Nodes as X (HNodes(..), HWitness(..), _HWitness, (#>), (#*#))-import Hyper.Class.Pointed as X (HPointed(..))-import Hyper.Class.Recursive as X (Recursively(..), RNodes, RTraversable)-import Hyper.Class.Traversable as X (HTraversable(..), htraverse, htraverse1)-import Hyper.Combinator.Ann as X+import Data.Constraint as X (Constraint, Dict (..), withDict)+import Data.Functor.Const as X (Const (..))+import Data.Proxy as X (Proxy (..))+import GHC.Generics as X (Generic, (:*:) (..))+import Hyper.Class.Apply as X (HApplicative, HApply (..), liftH2)+import Hyper.Class.Foldable as X (HFoldable (..), hfoldMap, hfolded1, htraverse1_, htraverse_)+import Hyper.Class.Functor as X (HFunctor (..), hmapped1)+import Hyper.Class.HasPlain as X (HasHPlain (..))+import Hyper.Class.Nodes as X (HNodes (..), HWitness (..), (#*#), (#>), _HWitness)+import Hyper.Class.Pointed as X (HPointed (..))+import Hyper.Class.Recursive as X (RNodes, RTraversable, Recursively (..))+import Hyper.Class.Traversable as X (HTraversable (..), htraverse, htraverse1) import Hyper.Combinator.ANode as X-import Hyper.Combinator.Compose as X (HCompose(..), _HCompose, hcomposed)+import Hyper.Combinator.Ann as X+import Hyper.Combinator.Compose as X (HCompose (..), hcomposed, _HCompose) import Hyper.Combinator.Flip as X import Hyper.Combinator.Func as X import Hyper.TH.Apply as X (makeHApplicativeBases) import Hyper.TH.Context as X (makeHContext) import Hyper.TH.HasPlain as X (makeHasHPlain) import Hyper.TH.Morph as X (makeHMorph)-import Hyper.TH.Traversable as X (makeHTraversableApplyAndBases, makeHTraversableAndBases)+import Hyper.TH.Traversable as X (makeHTraversableAndBases, makeHTraversableApplyAndBases) import Hyper.TH.ZipMatch as X (makeZipMatch) import Hyper.Type as X import Hyper.Type.Pure as X

@@ -1,11 +1,11 @@ -- | A variant of 'Data.Functor.Apply.Apply' for 'Hyper.Type.HyperType's- module Hyper.Class.Apply-    ( HApply(..), HApplicative+    ( HApply (..)+    , HApplicative     , liftH2     ) where -import Hyper.Class.Functor (HFunctor(..))+import Hyper.Class.Functor (HFunctor (..)) import Hyper.Class.Nodes (HWitness) import Hyper.Class.Pointed (HPointed) import Hyper.Type (type (#))

@@ -1,20 +1,22 @@-{-# LANGUAGE FlexibleContexts, FlexibleInstances #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}  module Hyper.Class.Context-    ( HContext(..)-    , recursiveContexts, annContexts+    ( HContext (..)+    , recursiveContexts+    , annContexts     ) where -import Control.Lens (mapped, from, _Wrapped, _1, _2)-import Hyper.Combinator.Compose (HCompose(..), _HCompose, decompose)-import Hyper.Combinator.Flip-import Hyper.Combinator.Func (HFunc(..), _HFunc)-import Hyper.Class.Functor (HFunctor(..))+import Control.Lens (from, mapped, _1, _2, _Wrapped)+import Hyper.Class.Functor (HFunctor (..)) import Hyper.Class.Nodes ((#*#), (#>))-import Hyper.Class.Recursive (Recursively(..))-import Hyper.Combinator.Ann (Ann(..))+import Hyper.Class.Recursive (Recursively (..))+import Hyper.Combinator.Ann (Ann (..))+import Hyper.Combinator.Compose (HCompose (..), decompose, _HCompose)+import Hyper.Combinator.Flip+import Hyper.Combinator.Func (HFunc (..), _HFunc) import Hyper.Type (type (#))-import Hyper.Type.Pure (Pure(..), _Pure)+import Hyper.Type.Pure (Pure (..), _Pure)  import Hyper.Internal.Prelude @@ -25,26 +27,24 @@         h # (HFunc p (Const (h # p)) :*: p)  instance HContext Pure where-    hcontext = _Pure %~ \x -> HFunc (Const . Pure) :*: x+    hcontext = _Pure %~ (HFunc (Const . Pure) :*:)  instance (HContext a, HFunctor a) => HContext (Ann a) where     hcontext (Ann a b) =         Ann-        (hmap (const (_1 . _HFunc . mapped . _Wrapped %~ (`Ann` b))) (hcontext a))-        (HFunc (Const . Ann a) :*: b)+            (hmap (const (_1 . _HFunc . mapped . _Wrapped %~ (`Ann` b))) (hcontext a))+            (HFunc (Const . Ann a) :*: b) -instance (HFunctor h0, HContext h0, HFunctor h1, HContext h1) => HContext (HCompose h0 h1) where+instance (HFunctor c1, HContext c1, HFunctor h1, HContext h1) => HContext (HCompose c1 h1) where     hcontext =-        _HCompose %~-        hmap-        ( \_ (HFunc c0 :*: x0) ->-            x0 & _HCompose %~-            hmap-            ( \_ (HFunc c1 :*: x1) ->-                x1 & _HCompose %~-                (HFunc (Const . (_HCompose #) . getConst . c0 . (_HCompose #) . getConst . c1 . (_HCompose #)) :*:)-            ) . hcontext-        ) . hcontext+        _HCompose %~ layer (\c0 -> layer $ \c1 -> (HFunc ((_Wrapped %~ (_HCompose #)) . c0 . getConst . c1) :*:))+        where+            layer ::+                (HFunctor h, HContext h) =>+                (forall n. (p0 # HCompose q0 n -> Const (h # HCompose p0 q0) # n) -> p0 # HCompose q0 n -> p1 # HCompose q1 n) ->+                (h # HCompose p0 q0) ->+                h # HCompose p1 q1+            layer f = hmap (\_ (HFunc c :*: x) -> x & _HCompose %~ f (c . (_HCompose #))) . hcontext  instance (Recursively HContext h, Recursively HFunctor h) => HContext (HFlip Ann h) where     -- The context of (HFlip Ann h) differs from annContexts in that@@ -55,16 +55,19 @@             f ::                 forall n p r.                 Recursively HFunctor n =>-                Ann (HFunc (Ann p) (Const r) :*: p) # n -> Ann (HFunc p (Const r) :*: p) # n+                Ann (HFunc (Ann p) (Const r) :*: p) # n ->+                Ann (HFunc p (Const r) :*: p) # n             f (Ann (HFunc func :*: a) b) =-                withDict (recursively (Proxy @(HFunctor n))) $                 Ann (HFunc (func . (`Ann` g b)) :*: a) (hmap (Proxy @(Recursively HFunctor) #> f) b)+                    \\ recursively (Proxy @(HFunctor n))             g ::                 forall n a b.-                Recursively HFunctor n => n # Ann (a :*: b) -> n # Ann b+                Recursively HFunctor n =>+                n # Ann (a :*: b) ->+                n # Ann b             g =-                withDict (recursively (Proxy @(HFunctor n))) $                 hmap (Proxy @(Recursively HFunctor) #> hflipped %~ hmap (const (^. _2)))+                    \\ recursively (Proxy @(HFunctor n))  -- | Add in the node annotations a function to replace each node in the top-level node recursiveContexts ::@@ -79,25 +82,24 @@     (HFunc p (Const r) :*: p) # h ->     HCompose (Ann (HFunc Pure (Const r))) p # h recursiveContextsWith (HFunc s0 :*: x0) =-    withDict (recursively (Proxy @(HFunctor p))) $-    withDict (recursively (Proxy @(HFunctor h))) $-    withDict (recursively (Proxy @(HContext p))) $-    withDict (recursively (Proxy @(HContext h))) $-    _HCompose # Ann-    { _hAnn = _HFunc # Const . getConst . s0 . (^. decompose)-    , _hVal =-        _HCompose #-        hmap-        ( Proxy @(Recursively HContext) #*# Proxy @(Recursively HFunctor) #>-            \(HFunc s1 :*: x1) ->-            _HCompose #-            hmap-            ( Proxy @(Recursively HContext) #*# Proxy @(Recursively HFunctor) #>-                \(HFunc s2 :*: x2) ->-                recursiveContextsWith (HFunc (Const . getConst . s0 . getConst . s1 . getConst . s2) :*: x2)-            ) (hcontext x1)-        ) (hcontext x0)-    }+    _HCompose+        # Ann+            { _hAnn = _HFunc # Const . getConst . s0 . (^. decompose)+            , _hVal =+                layer x0 $ \s1 x1 -> layer x1 $ \s2 x2 -> recursiveContextsWith (HFunc (Const . getConst . s0 . s1 . s2) :*: x2)+            }+    where+        layer ::+            forall t s c0 c1.+            (Recursively HFunctor t, Recursively HContext t) =>+            t # s ->+            (forall n. (Recursively HFunctor n, Recursively HContext n) => (s # n -> t # s) -> s # n -> HCompose c0 c1 # n) ->+            HCompose t c0 # c1+        layer x f =+            _HCompose+                # hmap (Proxy @(Recursively HContext) #*# Proxy @(Recursively HFunctor) #> \(HFunc s :*: v) -> f (getConst . s) v) (hcontext x)+                \\ recursively (Proxy @(HFunctor t))+                \\ recursively (Proxy @(HContext t))  -- | Add in the node annotations a function to replace each node in the top-level node --@@ -114,14 +116,16 @@     (HFunc (Ann p) (Const r) :*: Ann p) # h ->     Ann (HFunc (Ann p) (Const r) :*: p) # h annContextsWith (HFunc s0 :*: Ann a b) =-    withDict (recursively (Proxy @(HContext h))) $-    withDict (recursively (Proxy @(HFunctor h)))     Ann-    { _hAnn = HFunc s0 :*: a-    , _hVal =-        hmap-        ( Proxy @(Recursively HContext) #*# Proxy @(Recursively HFunctor) #>-            \(HFunc s1 :*: x) ->-            annContextsWith (HFunc (Const . getConst . s0 . Ann a . getConst . s1) :*: x)-        ) (hcontext b)-    }+        { _hAnn = HFunc s0 :*: a+        , _hVal =+            hmap+                ( Proxy @(Recursively HContext) #*#+                    Proxy @(Recursively HFunctor) #>+                        \(HFunc s1 :*: x) ->+                            annContextsWith (HFunc (Const . getConst . s0 . Ann a . getConst . s1) :*: x)+                )+                (hcontext b)+                \\ recursively (Proxy @(HFunctor h))+                \\ recursively (Proxy @(HContext h))+        }

@@ -1,16 +1,16 @@--- | A variant of 'Foldable' for 'Hyper.Type.HyperType's- {-# LANGUAGE FlexibleContexts #-} +-- | A variant of 'Foldable' for 'Hyper.Type.HyperType's module Hyper.Class.Foldable-    ( HFoldable(..)+    ( HFoldable (..)     , hfolded1-    , htraverse_, htraverse1_+    , htraverse_+    , htraverse1_     ) where  import Control.Lens (Fold, folding) import GHC.Generics-import Hyper.Class.Nodes (HNodes(..), HWitness(..), _HWitness, (#>))+import Hyper.Class.Nodes (HNodes (..), HWitness (..), (#>), _HWitness) import Hyper.Type (type (#))  import Hyper.Internal.Prelude@@ -28,7 +28,9 @@         a     {-# INLINE hfoldMap #-}     default hfoldMap ::-        ( Generic1 h, HFoldable (Rep1 h), HWitnessType h ~ HWitnessType (Rep1 h)+        ( Generic1 h+        , HFoldable (Rep1 h)+        , HWitnessType h ~ HWitnessType (Rep1 h)         , Monoid a         ) =>         (forall n. HWitness h n -> p # n -> a) ->@@ -38,13 +40,13 @@  instance HFoldable (Const a) where     {-# INLINE hfoldMap #-}-    hfoldMap _ _ = mempty+    hfoldMap _ = mempty  instance (HFoldable a, HFoldable b) => HFoldable (a :*: b) where     {-# INLINE hfoldMap #-}     hfoldMap f (x :*: y) =-        hfoldMap (f . HWitness . L1) x <>-        hfoldMap (f . HWitness . R1) y+        hfoldMap (f . HWitness . L1) x+            <> hfoldMap (f . HWitness . R1) y  instance (HFoldable a, HFoldable b) => HFoldable (a :+: b) where     {-# INLINE hfoldMap #-}@@ -77,13 +79,14 @@     (forall c. HWitness h c -> m # c -> f ()) ->     h # m ->     f ()-htraverse_ f = sequenceA_ . hfoldMap (fmap (:[]) . f)+htraverse_ f = sequenceA_ . hfoldMap (fmap (: []) . f)  -- | 'HFoldable' variant of 'Data.Foldable.traverse_' for 'Hyper.Type.HyperType's with a single node type (avoids using @RankNTypes@) {-# INLINE htraverse1_ #-} htraverse1_ ::     forall f h n p.-    ( Applicative f, HFoldable h+    ( Applicative f+    , HFoldable h     , HNodesConstraint h ((~) n)     ) =>     (p # n -> f ()) ->

@@ -1,16 +1,16 @@--- | A variant of 'Functor' for 'Hyper.Type.HyperType's- {-# LANGUAGE FlexibleContexts #-} +-- | A variant of 'Functor' for 'Hyper.Type.HyperType's module Hyper.Class.Functor-    ( HFunctor(..)+    ( HFunctor (..)     , hmapped1     , hiso     ) where -import Control.Lens (Setter, Iso', AnIso', sets, iso, cloneIso)+import Control.Lens (AnIso', Iso', Setter, cloneIso, iso, sets, _Wrapped) import GHC.Generics-import Hyper.Class.Nodes (HNodes(..), HWitness(..), _HWitness, (#>))+import GHC.Generics.Lens (generic1)+import Hyper.Class.Nodes (HNodes (..), HWitness (..), (#>), _HWitness) import Hyper.Type (type (#))  import Hyper.Internal.Prelude@@ -31,17 +31,17 @@         (forall n. HWitness h n -> p # n -> q # n) ->         h # p ->         h # q-    hmap f = to1 . hmap (f . (_HWitness %~ id)) . from1+    hmap f = generic1 %~ hmap (f . (_HWitness %~ id))  instance HFunctor (Const a) where     {-# INLINE hmap #-}-    hmap _ (Const x) = Const x+    hmap _ = _Wrapped %~ id  instance (HFunctor a, HFunctor b) => HFunctor (a :*: b) where     {-# INLINE hmap #-}     hmap f (x :*: y) =-        hmap (f . HWitness . L1) x :*:-        hmap (f . HWitness . R1) y+        hmap (f . HWitness . L1) x+            :*: hmap (f . HWitness . R1) y  instance (HFunctor a, HFunctor b) => HFunctor (a :+: b) where     {-# INLINE hmap #-}

@@ -1,12 +1,11 @@+{-# LANGUAGE FlexibleContexts #-}+ -- | A class for plain 'Data.Kind.Type' equivalents -- for the simple forms of 'Hyper.Type.HyperType's. -- -- Useful for succinct tests, examples, and for debug prints.--{-# LANGUAGE FlexibleContexts #-}- module Hyper.Class.HasPlain-    ( HasHPlain(..)+    ( HasHPlain (..)     ) where  import Control.Lens (Iso')@@ -19,5 +18,6 @@ class Show (HPlain h) => HasHPlain h where     -- | Plain form data type     data HPlain h+     -- | An 'Control.Lens.Iso' between the plain form and 'Hyper.Type.HyperType' form     hPlain :: Iso' (HPlain h) (Pure # h)

@@ -1,19 +1,24 @@-{-# LANGUAGE TemplateHaskell, FlexibleInstances, FlexibleContexts #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE TemplateHaskell #-}  module Hyper.Class.Infer     ( InferOf-    , Infer(..)-    , InferChild(..), _InferChild-    , InferredChild(..), inType, inRep+    , Infer (..)+    , InferChild (..)+    , _InferChild+    , InferredChild (..)+    , inType+    , inRep     ) where  import qualified Control.Lens as Lens-import           GHC.Generics-import           Hyper-import           Hyper.Class.Unify-import           Hyper.Recurse+import GHC.Generics+import Hyper+import Hyper.Class.Unify+import Hyper.Recurse -import           Hyper.Internal.Prelude+import Hyper.Internal.Prelude  -- | @InferOf e@ is the inference result of @e@. --@@ -30,22 +35,23 @@ -- | A 'HyperType' containing an inferred child node data InferredChild v h t = InferredChild     { _inRep :: !(h t)-        -- ^ Inferred node.-        ---        -- An 'inferBody' implementation needs to place this value in the corresponding child node of the inferred term body+    -- ^ Inferred node.+    --+    -- An 'inferBody' implementation needs to place this value in the corresponding child node of the inferred term body     , _inType :: !(InferOf (GetHyperType t) # v)-        -- ^ The inference result for the child node.-        ---        -- An 'inferBody' implementation may use it to perform unifications with it.+    -- ^ The inference result for the child node.+    --+    -- An 'inferBody' implementation may use it to perform unifications with it.     }+ makeLenses ''InferredChild  -- | A 'HyperType' containing an inference action. -- -- The caller may modify the scope before invoking the action via -- 'Hyper.Class.Infer.Env.localScopeType' or 'Hyper.Infer.ScopeLevel.localLevel'-newtype InferChild m h t =-    InferChild { inferChild :: m (InferredChild (UVarOf m) h t) }+newtype InferChild m h t = InferChild {inferChild :: m (InferredChild (UVarOf m) h t)}+ makePrisms ''InferChild  -- | @Infer m t@ enables 'Hyper.Infer.infer' to perform type-inference for @t@ in the 'Monad' @m@.@@ -87,8 +93,7 @@  instance Recursive (Infer m) where     {-# INLINE recurse #-}-    recurse p =-        withDict (inferContext (Proxy @m) (proxyArgument p)) Dict+    recurse p = Dict \\ inferContext (Proxy @m) (proxyArgument p)  type instance InferOf (a :+: _) = InferOf a @@ -98,9 +103,7 @@     inferBody (R1 x) = inferBody x <&> Lens._1 %~ R1      {-# INLINE inferContext #-}-    inferContext p _ =-        withDict (inferContext p (Proxy @a)) $-        withDict (inferContext p (Proxy @b)) Dict+    inferContext p _ = Dict \\ inferContext p (Proxy @a) \\ inferContext p (Proxy @b)  type instance InferOf (M1 _ _ h) = InferOf h @@ -109,7 +112,7 @@     inferBody (M1 x) = inferBody x <&> Lens._1 %~ M1      {-# INLINE inferContext #-}-    inferContext p _ = withDict (inferContext p (Proxy @h)) Dict+    inferContext p _ = Dict \\ inferContext p (Proxy @h)  type instance InferOf (Rec1 h) = InferOf h @@ -118,4 +121,4 @@     inferBody (Rec1 x) = inferBody x <&> Lens._1 %~ Rec1      {-# INLINE inferContext #-}-    inferContext p _ = withDict (inferContext p (Proxy @h)) Dict+    inferContext p _ = Dict \\ inferContext p (Proxy @h)

@@ -1,7 +1,6 @@ -- | Traits of inference monads.- module Hyper.Class.Infer.Env-    ( LocalScopeType(..)+    ( LocalScopeType (..)     ) where  -- | @LocalScopeType var scheme m@ represents that

@@ -1,18 +1,15 @@-{-# LANGUAGE FlexibleContexts, FlexibleInstances, UndecidableInstances #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE UndecidableInstances #-}  module Hyper.Class.Infer.InferOf-    ( HasInferredType(..)-    , HasInferredValue(..)-    , InferOfConstraint(..), RTraversableInferOf+    ( HasInferredType (..)+    , HasInferredValue (..)+    , InferOfConstraint (..)     ) where  import Control.Lens (ALens', Lens')-import Hyper.Class.Foldable (HFoldable)-import Hyper.Class.Functor (HFunctor) import Hyper.Class.Infer (InferOf)-import Hyper.Class.Nodes (HNodes(..))-import Hyper.Class.Recursive (Recursive(..), Recursively, proxyArgument)-import Hyper.Class.Traversable (HTraversable) import Hyper.Type (HyperType, type (#))  import Hyper.Internal.Prelude@@ -21,6 +18,7 @@ class HasInferredType t where     -- | The type of @t@     type TypeOf t :: HyperType+     -- A 'Control.Lens.Lens' from an inference result to an inferred type     inferredType :: Proxy t -> ALens' (InferOf t # v) (v # TypeOf t) @@ -30,22 +28,7 @@     inferredValue :: Lens' (InferOf t # v) (v # t)  class InferOfConstraint c h where-    inferOfConstraint :: proxy0 c -> proxy1 h -> Dict (c (InferOf h))+    inferOfConstraint :: proxy h -> Dict (c (InferOf h))  instance c (InferOf h) => InferOfConstraint c h where-    inferOfConstraint _ _ = Dict--class-    (HTraversable (InferOf h), Recursively (InferOfConstraint HFunctor) h, Recursively (InferOfConstraint HFoldable) h) =>-    RTraversableInferOf h where-    rTraversableInferOfRec ::-        Proxy h -> Dict (HNodesConstraint h RTraversableInferOf)-    {-# INLINE rTraversableInferOfRec #-}-    default rTraversableInferOfRec ::-        HNodesConstraint h RTraversableInferOf =>-        Proxy h -> Dict (HNodesConstraint h RTraversableInferOf)-    rTraversableInferOfRec _ = Dict--instance Recursive RTraversableInferOf where-    {-# INLINE recurse #-}-    recurse = rTraversableInferOfRec . proxyArgument+    inferOfConstraint _ = Dict

@@ -1,18 +1,18 @@--- | A variant of 'Control.Monad.Monad' for 'Hyper.Type.HyperType's- {-# LANGUAGE FlexibleContexts #-} +-- | A variant of 'Control.Monad.Monad' for 'Hyper.Type.HyperType's module Hyper.Class.Monad-    ( HMonad(..), hbind+    ( HMonad (..)+    , hbind     ) where  import Hyper.Class.Apply (HApplicative)-import Hyper.Class.Functor (HFunctor(..))+import Hyper.Class.Functor (HFunctor (..)) import Hyper.Class.Nodes (HWitness, (#>))-import Hyper.Class.Recursive (Recursively(..))+import Hyper.Class.Recursive (Recursively (..)) import Hyper.Combinator.Compose (HCompose, _HCompose) import Hyper.Type (type (#))-import Hyper.Type.Pure (Pure(..), _Pure)+import Hyper.Type.Pure (Pure (..), _Pure)  import Hyper.Internal.Prelude @@ -25,10 +25,11 @@  instance HMonad Pure where     hjoin x =-        withDict (recursively (p x)) $-        _Pure #-        hmap (Proxy @(Recursively HFunctor) #> hjoin)-        (x ^. _HCompose . _Pure . _HCompose . _Pure . _HCompose)+        _Pure+            # hmap+                (Proxy @(Recursively HFunctor) #> hjoin)+                (x ^. _HCompose . _Pure . _HCompose . _Pure . _HCompose)+            \\ recursively (p x)         where             p :: HCompose Pure Pure # p -> Proxy (HFunctor p)             p _ = Proxy

@@ -1,17 +1,20 @@ {-# LANGUAGE FlexibleInstances #-}  -- | An extension of 'HFunctor' for parameterized 'Hyper.Type.HyperType's- module Hyper.Class.Morph-    ( HMorph(..), HMorphWithConstraint-    , morphTraverse, (#?>)-    , HIs2, morphMapped1, morphTraverse1+    ( HMorph (..)+    , HMorphWithConstraint+    , morphTraverse+    , (#?>)+    , HIs2+    , morphMapped1+    , morphTraverse1     ) where  import Control.Lens (Setter, sets) import Data.Kind (Type)-import Hyper.Class.Traversable (HTraversable(..), ContainedH(..))-import Hyper.Type (type (#), HyperType)+import Hyper.Class.Traversable (ContainedH (..), HTraversable (..))+import Hyper.Type (HyperType, type (#))  import Hyper.Internal.Prelude @@ -45,7 +48,10 @@  (#?>) ::     (HMorph s t, MorphConstraint s t c) =>-    Proxy c -> (c a b => r) -> MorphWitness s t a b -> r+    Proxy c ->+    (c a b => r) ->+    MorphWitness s t a b ->+    r (#?>) p r w = morphLiftConstraint w p r  class (i0 ~ t0, i1 ~ t1) => HIs2 (i0 :: HyperType) (i1 :: HyperType) t0 t1

@@ -1,12 +1,17 @@--- | A class for witness types and lifting of constraints to the child nodes of a 'HyperType'--{-# LANGUAGE EmptyCase, UndecidableInstances, TemplateHaskell, FlexibleContexts #-}+{-# LANGUAGE EmptyCase #-}+{-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE UndecidableInstances #-} +-- | A class for witness types and lifting of constraints to the child nodes of a 'HyperType' module Hyper.Class.Nodes-    ( HNodes(..), HWitness(..), _HWitness-    , (#>), (#*#)-    , HNodesHaveConstraint(..)+    ( HNodes (..)+    , HWitness (..)+    , _HWitness+    , (#>)+    , (#*#)+    , HNodesHaveConstraint (..)     ) where  import Data.Kind (Type)@@ -25,15 +30,17 @@ class HNodes (h :: HyperType) where     -- | Lift a constraint to apply to the child nodes     type HNodesConstraint h (c :: (HyperType -> Constraint)) :: Constraint-    type instance HNodesConstraint h c = HNodesConstraint (Rep1 h) c +    type HNodesConstraint h c = HNodesConstraint (Rep1 h) c+     -- | @HWitness h n@ is a witness that @n@ is a node of @h@.     --     -- A value quantified with @forall n. HWitness h n -> ... n@,     -- is equivalent for a "for-some" where the possible values for @n@ are the nodes of @h@.     type HWitnessType h :: HyperType -> Type-    type instance HWitnessType h = HWitnessType (Rep1 h) +    type HWitnessType h = HWitnessType (Rep1 h)+     -- | Lift a rank-n value with a constraint which the child nodes satisfy     -- to a function from a node witness.     hLiftConstraint ::@@ -61,7 +68,7 @@     type HNodesConstraint (Const a) _ = ()     type HWitnessType (Const a) = V1     {-# INLINE hLiftConstraint #-}-    hLiftConstraint = \case{}+    hLiftConstraint = \case {}  instance (HNodes a, HNodes b) => HNodes (a :*: b) where     type HNodesConstraint (a :*: b) x = (HNodesConstraint a x, HNodesConstraint b x)@@ -87,7 +94,10 @@ {-# INLINE (#>) #-} (#>) ::     (HNodes h, HNodesConstraint h c) =>-    Proxy c -> (c n => r) -> HWitness h n -> r+    Proxy c ->+    (c n => r) ->+    HWitness h n ->+    r (#>) p r w = hLiftConstraint w p r  -- | A variant of '#>' which does not consume the witness parameter.@@ -96,7 +106,10 @@ {-# INLINE (#*#) #-} (#*#) ::     (HNodes h, HNodesConstraint h c) =>-    Proxy c -> (c n => HWitness h n -> r) -> HWitness h n -> r+    Proxy c ->+    (c n => HWitness h n -> r) ->+    HWitness h n ->+    r (#*#) p r w = (p #> r) w w  -- | Defunctionalized HNodesConstraint which can be curried

@@ -1,8 +1,9 @@ {-# LANGUAGE FlexibleContexts #-}  module Hyper.Class.Optic-    ( HNodeLens(..)-    , HSubset(..), HSubset'+    ( HNodeLens (..)+    , HSubset (..)+    , HSubset'     ) where  import Control.Lens (Lens', Prism)

@@ -1,11 +1,10 @@ -- | A variant of 'Data.Pointed.Pointed' for 'Hyper.Type.HyperType's- module Hyper.Class.Pointed-    ( HPointed(..)+    ( HPointed (..)     ) where -import GHC.Generics ((:+:)(..))-import Hyper.Class.Nodes (HNodes, HWitness(..))+import GHC.Generics ((:+:) (..))+import Hyper.Class.Nodes (HNodes, HWitness (..)) import Hyper.Type (type (#))  import Hyper.Internal.Prelude

@@ -1,20 +1,23 @@--- | Classes applying on 'HyperType's recursively--{-# LANGUAGE FlexibleContexts, FlexibleInstances #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-} +-- | Classes applying on 'HyperType's recursively module Hyper.Class.Recursive-    ( Recursive(..)-    , Recursively(..)-    , RNodes(..), RTraversable(..)+    ( Recursive (..)+    , Recursively (..)+    , RNodes (..)+    , RTraversable (..)+    , RecMethod+    , DefRecMethod     , proxyArgument     ) where  import Hyper.Class.Foldable-import Hyper.Class.Functor (HFunctor(..))-import Hyper.Class.Nodes (HNodes(..))+import Hyper.Class.Functor (HFunctor (..))+import Hyper.Class.Nodes (HNodes (..)) import Hyper.Class.Traversable import Hyper.Type-import Hyper.Type.Pure (Pure(..))+import Hyper.Type.Pure (Pure (..))  import Hyper.Internal.Prelude @@ -23,13 +26,14 @@     -- | Lift a recursive constraint to the next layer     recurse :: (HNodes h, c h) => proxy (c h) -> Dict (HNodesConstraint h c) +type RecMethod c h = Proxy h -> Dict (HNodesConstraint h c)+type DefRecMethod c h = HNodesConstraint h c => RecMethod c h+ -- | A class of 'HyperType's which recursively implement 'HNodes' class HNodes h => RNodes h where-    recursiveHNodes :: proxy h -> Dict (HNodesConstraint h RNodes)+    recursiveHNodes :: RecMethod RNodes h     {-# INLINE recursiveHNodes #-}-    default recursiveHNodes ::-        HNodesConstraint h RNodes =>-        proxy h -> Dict (HNodesConstraint h RNodes)+    default recursiveHNodes :: DefRecMethod RNodes h     recursiveHNodes _ = Dict  instance RNodes Pure@@ -49,18 +53,18 @@ -- one will want to create a class such as RTraversable to capture the dependencies, -- otherwise using it in class contexts will be quite unergonomic. class RNodes h => Recursively c h where-    recursively ::-        proxy (c h) -> Dict (c h, HNodesConstraint h (Recursively c))+    recursively :: proxy (c h) -> Dict (c h, HNodesConstraint h (Recursively c))     {-# INLINE recursively #-}     default recursively ::         (c h, HNodesConstraint h (Recursively c)) =>-        proxy (c h) -> Dict (c h, HNodesConstraint h (Recursively c))+        proxy (c h) ->+        Dict (c h, HNodesConstraint h (Recursively c))     recursively _ = Dict  instance Recursive (Recursively c) where     {-# INLINE recurse #-}     recurse p =-        withDict (recursively (p0 p)) Dict+        Dict \\ recursively (p0 p)         where             p0 :: proxy (Recursively c h) -> Proxy (c h)             p0 _ = Proxy@@ -70,11 +74,9 @@  -- | A class of 'HyperType's which recursively implement 'HTraversable' class (HTraversable h, Recursively HFunctor h, Recursively HFoldable h) => RTraversable h where-    recursiveHTraversable :: proxy h -> Dict (HNodesConstraint h RTraversable)+    recursiveHTraversable :: RecMethod RTraversable h     {-# INLINE recursiveHTraversable #-}-    default recursiveHTraversable ::-        HNodesConstraint h RTraversable =>-        proxy h -> Dict (HNodesConstraint h RTraversable)+    default recursiveHTraversable :: DefRecMethod RTraversable h     recursiveHTraversable _ = Dict  instance RTraversable Pure

@@ -1,19 +1,20 @@--- | A variant of 'Traversable' for 'Hyper.Type.HyperType's- {-# LANGUAGE FlexibleContexts #-} +-- | A variant of 'Traversable' for 'Hyper.Type.HyperType's module Hyper.Class.Traversable-    ( HTraversable(..)-    , ContainedH(..), _ContainedH-    , htraverse, htraverse1+    ( HTraversable (..)+    , ContainedH (..)+    , _ContainedH+    , htraverse+    , htraverse1     ) where  import Control.Lens (iso) import GHC.Generics-import GHC.Generics.Lens (_M1, _Rec1)+import GHC.Generics.Lens (generic1, _M1, _Rec1) import Hyper.Class.Foldable (HFoldable)-import Hyper.Class.Functor (HFunctor(..), hmapped1)-import Hyper.Class.Nodes (HNodes(..), HWitness)+import Hyper.Class.Functor (HFunctor (..), hmapped1)+import Hyper.Class.Nodes (HNodes (..), HWitness) import Hyper.Type (AHyperType, type (#))  import Hyper.Internal.Prelude@@ -21,12 +22,13 @@ -- | A 'Hyper.Type.HyperType' containing a tree inside an action. -- -- Used to express 'hsequence'.-newtype ContainedH f p (h :: AHyperType) = MkContainedH { runContainedH :: f (p h) }+newtype ContainedH f p (h :: AHyperType) = MkContainedH {runContainedH :: f (p h)}  -- | An 'Iso' for the 'ContainedH' @newtype@ {-# INLINE _ContainedH #-} _ContainedH ::-    Iso (ContainedH f0 p0 # k0)+    Iso+        (ContainedH f0 p0 # k0)         (ContainedH f1 p1 # k1)         (f0 (p0 # k0))         (f1 (p1 # k1))@@ -44,7 +46,7 @@         (Generic1 h, HTraversable (Rep1 h), Applicative f) =>         h # ContainedH f p ->         f (h # p)-    hsequence = fmap to1 . hsequence . from1+    hsequence = generic1 hsequence  instance HTraversable (Const a) where     {-# INLINE hsequence #-}

@@ -1,30 +1,32 @@--- | A class for unification- {-# LANGUAGE FlexibleContexts #-} +-- | A class for unification module Hyper.Class.Unify-    ( Unify(..), UVarOf-    , UnifyGen(..)-    , BindingDict(..)-    , applyBindings, semiPruneLookup, occursError+    ( Unify (..)+    , UVarOf+    , UnifyGen (..)+    , BindingDict (..)+    , applyBindings+    , semiPruneLookup+    , occursError     ) where  import Control.Monad (unless)-import Control.Monad.Error.Class (MonadError(..))-import Control.Monad.Trans.Class (MonadTrans(..))-import Control.Monad.Trans.State (runStateT, get, put)+import Control.Monad.Error.Class (MonadError (..))+import Control.Monad.Trans.Class (MonadTrans (..))+import Control.Monad.Trans.State (get, put, runStateT) import Data.Kind (Type)-import Hyper.Class.Nodes (HNodes(..), (#>))-import Hyper.Class.Optic (HSubset(..), HSubset')+import Hyper.Class.Nodes (HNodes (..), (#>))+import Hyper.Class.Optic (HSubset (..), HSubset') import Hyper.Class.Recursive import Hyper.Class.Traversable (htraverse) import Hyper.Class.ZipMatch (ZipMatch) import Hyper.Type (HyperType, type (#)) import Hyper.Type.Pure (Pure, _Pure) import Hyper.Unify.Constraints-import Hyper.Unify.Error (UnifyError(..))-import Hyper.Unify.QuantifiedVar (MonadQuantify(..), HasQuantifiedVar(..))-import Hyper.Unify.Term (UTerm(..), UTermBody(..), uBody)+import Hyper.Unify.Error (UnifyError (..))+import Hyper.Unify.QuantifiedVar (HasQuantifiedVar (..), MonadQuantify (..))+import Hyper.Unify.Term (UTerm (..), UTermBody (..), uBody)  import Hyper.Internal.Prelude @@ -61,8 +63,9 @@     , HasQuantifiedVar t     , Monad m     , MonadQuantify (TypeConstraintsOf t) (QVar t) m-    ) => Unify m t where-+    ) =>+    Unify m t+    where     -- | The implementation for unification variables binding and lookup     binding :: BindingDict (UVarOf m) m t @@ -73,11 +76,13 @@     unifyError :: UnifyError t # UVarOf m -> m a     default unifyError ::         (MonadError (e # Pure) m, HSubset' e (UnifyError t)) =>-        UnifyError t # UVarOf m -> m a+        UnifyError t # UVarOf m ->+        m a     unifyError e =-        withDict (unifyRecursive (Proxy @m) (Proxy @t)) $         htraverse (Proxy @(Unify m) #> applyBindings) e-        >>= throwError . (hSubset #)+            >>= throwError+                . (hSubset #)+            \\ unifyRecursive (Proxy @m) (Proxy @t)      -- | What to do when top-levels of terms being unified do not match.     --@@ -88,15 +93,15 @@     -- Those would override the default implementation to handle the unification of mismatching structures.     structureMismatch ::         (forall c. Unify m c => UVarOf m # c -> UVarOf m # c -> m (UVarOf m # c)) ->-        t # UVarOf m -> t # UVarOf m -> m ()+        t # UVarOf m ->+        t # UVarOf m ->+        m ()     structureMismatch _ x y = unifyError (Mismatch x y)      -- TODO: Putting documentation here causes duplication in the haddock documentation-    unifyRecursive :: Proxy m -> Proxy t -> Dict (HNodesConstraint t (Unify m))+    unifyRecursive :: Proxy m -> RecMethod (Unify m) t     {-# INLINE unifyRecursive #-}-    default unifyRecursive ::-        HNodesConstraint t (Unify m) =>-        Proxy m -> Proxy t -> Dict (HNodesConstraint t (Unify m))+    default unifyRecursive :: HNodesConstraint t (Unify m) => Proxy m -> RecMethod (Unify m) t     unifyRecursive _ _ = Dict  instance Recursive (Unify m) where@@ -108,11 +113,10 @@     -- | Get the current scope constraint     scopeConstraints :: Proxy t -> m (TypeConstraintsOf t) -    unifyGenRecursive :: Proxy m -> Proxy t -> Dict (HNodesConstraint t (UnifyGen m))+    unifyGenRecursive :: Proxy m -> RecMethod (UnifyGen m) t     {-# INLINE unifyGenRecursive #-}     default unifyGenRecursive ::-        HNodesConstraint t (UnifyGen m) =>-        Proxy m -> Proxy t -> Dict (HNodesConstraint t (UnifyGen m))+        HNodesConstraint t (UnifyGen m) => Proxy m -> RecMethod (UnifyGen m) t     unifyGenRecursive _ _ = Dict  instance Recursive (UnifyGen m) where@@ -129,14 +133,13 @@     m (UVarOf m # t, UTerm (UVarOf m) # t) semiPruneLookup v0 =     lookupVar binding v0-    >>=-    \case-    UToVar v1 ->-        do-            (v, r) <- semiPruneLookup v1-            bindVar binding v0 (UToVar v)-            pure (v, r)-    t -> pure (v0, t)+        >>= \case+            UToVar v1 ->+                do+                    (v, r) <- semiPruneLookup v1+                    bindVar binding v0 (UToVar v)+                    pure (v, r)+            t -> pure (v0, t)  -- | Resolve a term from a unification variable. --@@ -150,44 +153,46 @@     UVarOf m # t ->     m (Pure # t) applyBindings v0 =-    semiPruneLookup v0-    >>=-    \(v1, x) ->-    let result r = r <$ bindVar binding v1 (UResolved r)-        quantify c =-            newQuantifiedVariable c <&> (_Pure . quantifiedVar #)-            >>= result-    in-    case x of-    UResolving t -> occursError v1 t-    UResolved t -> pure t-    UUnbound c -> quantify c-    USkolem c -> quantify c-    UTerm b ->-        do-            (r, anyChild) <--                withDict (unifyRecursive (Proxy @m) (Proxy @t)) $-                htraverse-                ( Proxy @(Unify m) #>-                    \c ->-                    do-                        get >>= lift . (`unless` bindVar binding v1 (UResolving b))-                        put True-                        applyBindings c & lift-                ) (b ^. uBody)-                & (`runStateT` False)-            _Pure # r & if anyChild then result else pure-    UToVar{} -> error "lookup not expected to result in var"-    UConverted{} -> error "conversion state not expected in applyBindings"-    UInstantiated{} ->-        -- This can happen in alphaEq,-        -- where UInstantiated marks that var from one side matches var in the other.-        quantify mempty+    do+        (v1, x) <- semiPruneLookup v0+        let result r = r <$ bindVar binding v1 (UResolved r)+        let quantify c =+                newQuantifiedVariable c+                    <&> (_Pure . quantifiedVar #)+                    >>= result+        case x of+            UResolving t -> occursError v1 t+            UResolved t -> pure t+            UUnbound c -> quantify c+            USkolem c -> quantify c+            UTerm b ->+                do+                    (r, anyChild) <-+                        htraverse+                            ( Proxy @(Unify m) #>+                                \c ->+                                    do+                                        get >>= lift . (`unless` bindVar binding v1 (UResolving b))+                                        put True+                                        applyBindings c & lift+                            )+                            (b ^. uBody)+                            & (`runStateT` False)+                            \\ unifyRecursive (Proxy @m) (Proxy @t)+                    _Pure # r & if anyChild then result else pure+            UToVar{} -> error "lookup not expected to result in var"+            UConverted{} -> error "conversion state not expected in applyBindings"+            UInstantiated{} ->+                -- This can happen in alphaEq,+                -- where UInstantiated marks that var from one side matches var in the other.+                quantify mempty  -- | Format and throw an occurs check error occursError ::     Unify m t =>-    UVarOf m # t -> UTermBody (UVarOf m) # t -> m a+    UVarOf m # t ->+    UTermBody (UVarOf m) # t ->+    m a occursError v (UTermBody c b) =     do         q <- newQuantifiedVariable c

@@ -1,21 +1,22 @@--- | A class to match term structures- {-# LANGUAGE FlexibleContexts #-} +-- | A class to match term structures module Hyper.Class.ZipMatch-    ( ZipMatch(..)+    ( ZipMatch (..)     , zipMatch2     , zipMatchA-    , zipMatch_, zipMatch1_+    , zipMatch_+    , zipMatch1_     ) where  import GHC.Generics-import Hyper.Class.Foldable (HFoldable, htraverse_, htraverse1_)-import Hyper.Class.Functor (HFunctor(..))-import Hyper.Class.Nodes (HNodes(..), HWitness)+import GHC.Generics.Lens (generic1)+import Hyper.Class.Foldable (HFoldable, htraverse1_, htraverse_)+import Hyper.Class.Functor (HFunctor (..))+import Hyper.Class.Nodes (HNodes (..), HWitness) import Hyper.Class.Traversable (HTraversable, htraverse) import Hyper.Type (type (#))-import Hyper.Type.Pure (Pure(..), _Pure)+import Hyper.Type.Pure (Pure (..), _Pure)  import Hyper.Internal.Prelude @@ -37,9 +38,10 @@     zipMatch :: h # p -> h # q -> Maybe (h # (p :*: q))     default zipMatch ::         (Generic1 h, ZipMatch (Rep1 h)) =>-        h # p -> h # q -> Maybe (h # (p :*: q))-    zipMatch x =-        fmap to1 . zipMatch (from1 x) . from1+        h # p ->+        h # q ->+        Maybe (h # (p :*: q))+    zipMatch = generic1 . zipMatch . from1  instance ZipMatch Pure where     {-# INLINE zipMatch #-}@@ -68,7 +70,9 @@ zipMatch2 ::     (ZipMatch h, HFunctor h) =>     (forall n. HWitness h n -> p # n -> q # n -> r # n) ->-    h # p -> h # q -> Maybe (h # r)+    h # p ->+    h # q ->+    Maybe (h # r) zipMatch2 f x y = zipMatch x y <&> hmap (\w (a :*: b) -> f w a b)  -- | An 'Applicative' variant of 'zipMatch2'@@ -76,7 +80,9 @@ zipMatchA ::     (Applicative f, ZipMatch h, HTraversable h) =>     (forall n. HWitness h n -> p # n -> q # n -> f (r # n)) ->-    h # p -> h # q -> Maybe (f (h # r))+    h # p ->+    h # q ->+    Maybe (f (h # r)) zipMatchA f x y = zipMatch x y <&> htraverse (\w (a :*: b) -> f w a b)  -- | A variant of 'zipMatchA' where the 'Applicative' actions do not contain results@@ -84,7 +90,9 @@ zipMatch_ ::     (Applicative f, ZipMatch h, HFoldable h) =>     (forall n. HWitness h n -> p # n -> q # n -> f ()) ->-    h # p -> h # q -> Maybe (f ())+    h # p ->+    h # q ->+    Maybe (f ()) zipMatch_ f x y = zipMatch x y <&> htraverse_ (\w (a :*: b) -> f w a b)  -- | A variant of 'zipMatch_' for 'Hyper.Type.HyperType's with a single node type (avoids using @RankNTypes@)@@ -92,5 +100,7 @@ zipMatch1_ ::     (Applicative f, ZipMatch h, HFoldable h, HNodesConstraint h ((~) n)) =>     (p # n -> q # n -> f ()) ->-    h # p -> h # q -> Maybe (f ())+    h # p ->+    h # q ->+    Maybe (f ()) zipMatch1_ f x y = zipMatch x y <&> htraverse1_ (\(a :*: b) -> f a b)

@@ -1,15 +1,19 @@-{-# LANGUAGE UndecidableInstances, TemplateHaskell, FlexibleInstances #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE UndecidableInstances #-}  -- | A simple 'Hyper.Type.HyperType' with a single child node- module Hyper.Combinator.ANode-    ( ANode(..), _ANode, W_ANode(..), MorphWitness(..)+    ( ANode (..)+    , _ANode+    , W_ANode (..)+    , MorphWitness (..)     ) where  import Control.Lens (iso)-import Hyper.Class.Optic (HNodeLens(..))-import Hyper.Class.Morph (HMorph(..))-import Hyper.Class.Recursive (RNodes, Recursively, RTraversable)+import Hyper.Class.Morph (HMorph (..))+import Hyper.Class.Optic (HNodeLens (..))+import Hyper.Class.Recursive (RNodes, RTraversable, Recursively) import Hyper.TH.Traversable (makeHTraversableApplyAndBases) import Hyper.Type (type (#), type (:#)) @@ -17,7 +21,7 @@  -- | @ANode c@ is a 'Hyper.Type.HyperType' with a single child node of type @c@ newtype ANode c h = MkANode (h :# c)-    deriving stock Generic+    deriving stock (Generic)  -- | An 'Iso' from 'ANode' its child node. --@@ -37,8 +41,8 @@ instance RTraversable n => RTraversable (ANode n)  instance HMorph (ANode a) (ANode b) where-    type instance MorphConstraint (ANode a) (ANode b) c = c a b-    data instance MorphWitness (ANode a) (ANode b) _ _ where+    type MorphConstraint (ANode a) (ANode b) c = c a b+    data MorphWitness (ANode a) (ANode b) _ _ where         M_ANode :: MorphWitness (ANode a) (ANode b) a b     morphMap f = _ANode %~ f M_ANode     morphLiftConstraint M_ANode _ x = x

@@ -1,13 +1,20 @@-{-# LANGUAGE TemplateHaskell, UndecidableInstances, FlexibleInstances #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE UndecidableInstances #-}  module Hyper.Combinator.Ann-    ( Ann(..), hAnn, hVal-    , Annotated, annotation, annValue+    ( Ann (..)+    , hAnn+    , hVal+    , Annotated+    , annotation+    , annValue     ) where -import Control.Lens (Lens, Lens', _Wrapped, from)-import Hyper.Class.Foldable (HFoldable(..))-import Hyper.Class.Functor (HFunctor(..))+import Control.Lens (Lens, Lens', from, _Wrapped)+import Hyper.Class.Foldable (HFoldable (..))+import Hyper.Class.Functor (HFunctor (..)) import Hyper.Class.Nodes import Hyper.Class.Traversable import Hyper.Combinator.Flip@@ -20,7 +27,8 @@ data Ann a h = Ann     { _hAnn :: a h     , _hVal :: h :# Ann a-    } deriving Generic+    }+    deriving (Generic) makeLenses ''Ann  makeHTraversableApplyAndBases ''Ann@@ -36,61 +44,71 @@ hLiftConstraintH ::     forall a c b n r.     (RNodes a, HNodesConstraint (HFlip Ann a) c) =>-    HWitness a b -> HRecWitness b n -> Proxy c -> (c n => r) -> r+    HWitness a b ->+    HRecWitness b n ->+    Proxy c ->+    (c n => r) ->+    r hLiftConstraintH c n p f =-    withDict (recurse (Proxy @(RNodes a))) $-    withDict (recurse (Proxy @(c a))) $-    hLiftConstraint c (Proxy @RNodes)-    ( hLiftConstraint c p-        (hLiftConstraint (HWitness @(HFlip Ann _) n) p f)-    )+    hLiftConstraint+        c+        (Proxy @RNodes)+        ( hLiftConstraint+            c+            p+            (hLiftConstraint (HWitness @(HFlip Ann _) n) p f)+            \\ recurse (Proxy @(c a))+        )+        \\ recurse (Proxy @(RNodes a))  instance RNodes a => RNodes (Ann a) where     {-# INLINE recursiveHNodes #-}-    recursiveHNodes _ = withDict (recursiveHNodes (Proxy @a)) Dict+    recursiveHNodes _ = Dict \\ recursiveHNodes (Proxy @a)  instance (c (Ann a), Recursively c a) => Recursively c (Ann a) where     {-# INLINE recursively #-}-    recursively _ = withDict (recursively (Proxy @(c a))) Dict+    recursively _ = Dict \\ recursively (Proxy @(c a))  instance RTraversable a => RTraversable (Ann a) where     {-# INLINE recursiveHTraversable #-}-    recursiveHTraversable _ = withDict (recursiveHTraversable (Proxy @a)) Dict+    recursiveHTraversable _ = Dict \\ recursiveHTraversable (Proxy @a)  instance Recursively HFunctor h => HFunctor (HFlip Ann h) where     {-# INLINE hmap #-}     hmap f =-        withDict (recursively (Proxy @(HFunctor h))) $-        _HFlip %~-        \(Ann a b) ->-        Ann-        (f (HWitness HRecSelf) a)-        (hmap-            ( Proxy @(Recursively HFunctor) #*#-                \w -> from _HFlip %~ hmap (f . HWitness . HRecSub w . (^. _HWitness))-            ) b-        )+        _HFlip+            %~ \(Ann a b) ->+                Ann+                    (f (HWitness HRecSelf) a)+                    ( hmap+                        ( Proxy @(Recursively HFunctor) #*#+                            \w -> from _HFlip %~ hmap (f . HWitness . HRecSub w . (^. _HWitness))+                        )+                        b+                        \\ recursively (Proxy @(HFunctor h))+                    )  instance Recursively HFoldable h => HFoldable (HFlip Ann h) where     {-# INLINE hfoldMap #-}     hfoldMap f (MkHFlip (Ann a b)) =-        withDict (recursively (Proxy @(HFoldable h))) $-        f (HWitness HRecSelf) a <>-        hfoldMap-        ( Proxy @(Recursively HFoldable) #*#-            \w -> hfoldMap (f . HWitness . HRecSub w . (^. _HWitness)) . MkHFlip-        ) b+        f (HWitness HRecSelf) a+            <> hfoldMap+                ( Proxy @(Recursively HFoldable) #*#+                    \w -> hfoldMap (f . HWitness . HRecSub w . (^. _HWitness)) . MkHFlip+                )+                b+            \\ recursively (Proxy @(HFoldable h))  instance RTraversable h => HTraversable (HFlip Ann h) where     {-# INLINE hsequence #-}     hsequence =-        withDict (recurse (Proxy @(RTraversable h))) $         _HFlip-        ( \(Ann a b) ->-            Ann-            <$> runContainedH a-            <*> htraverse (Proxy @RTraversable #> from _HFlip hsequence) b-        )+            ( \(Ann a b) ->+                Ann+                    <$> runContainedH a+                    <*> htraverse (Proxy @RTraversable #> from _HFlip hsequence) b+                    \\ recurse (Proxy @(RTraversable h))+            )  type Annotated a = Ann (Const a) 

@@ -1,41 +1,54 @@+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE UndecidableInstances #-}+ -- | Compose two 'HyperType's. -- -- Inspired by [hyperfunctions' @Category@ instance](http://hackage.haskell.org/package/hyperfunctions-0/docs/Control-Monad-Hyper.html).--{-# LANGUAGE UndecidableInstances, FlexibleInstances, FlexibleContexts, TemplateHaskell #-}- module Hyper.Combinator.Compose-    ( HCompose(..), _HCompose, W_HCompose(..)+    ( HCompose (..)+    , _HCompose+    , W_HCompose (..)     , HComposeConstraint1-    , decompose, decompose', hcomposed+    , decompose+    , decompose'+    , hcomposed     ) where -import Control.Lens (Profunctor, Optic, Iso', iso)-import Hyper.Class.Apply (HApply(..))-import Hyper.Class.Foldable (HFoldable(..))-import Hyper.Class.Functor (HFunctor(..), hiso)-import Hyper.Class.Nodes (HNodes(..), HWitness(..), (#>))-import Hyper.Class.Pointed (HPointed(..))-import Hyper.Class.Traversable (HTraversable(..), ContainedH(..), htraverse)-import Hyper.Class.Recursive (RNodes(..), Recursively(..), RTraversable)-import Hyper.Class.ZipMatch (ZipMatch(..))-import Hyper.Type (HyperType, GetHyperType, type (#))+import Control.Lens (Iso', Optic, Profunctor, iso)+import Data.Constraint (withDict)+import Hyper.Class.Apply (HApply (..))+import Hyper.Class.Foldable (HFoldable (..))+import Hyper.Class.Functor (HFunctor (..), hiso)+import Hyper.Class.Nodes (HNodes (..), HWitness (..), (#>))+import Hyper.Class.Pointed (HPointed (..))+import Hyper.Class.Recursive (RNodes (..), RTraversable, Recursively (..))+import Hyper.Class.Traversable (ContainedH (..), HTraversable (..), htraverse)+import Hyper.Class.ZipMatch (ZipMatch (..))+import Hyper.Type (GetHyperType, HyperType, type (#)) import Hyper.Type.Pure (Pure, _Pure)+import Text.PrettyPrint.HughesPJClass (Pretty (..))  import Hyper.Internal.Prelude  -- | Compose two 'HyperType's as an external and internal layer-newtype HCompose a b h = HCompose { getHCompose :: a # HCompose b (GetHyperType h) }-    deriving stock Generic+newtype HCompose a b h = HCompose {getHCompose :: a # HCompose b (GetHyperType h)}+    deriving stock (Generic)  makeCommonInstances [''HCompose] +instance Pretty (a # HCompose b (GetHyperType h)) => Pretty (HCompose a b h) where+    pPrintPrec level prec (HCompose x) = pPrintPrec level prec x+ -- | An 'Control.Lens.Iso' for the 'HCompose' @newtype@ {-# INLINE _HCompose #-} _HCompose ::     Iso-    (HCompose a0 b0 # h0) (HCompose a1 b1 # h1)-    (a0 # HCompose b0 h0) (a1 # HCompose b1 h1)+        (HCompose a0 b0 # h0)+        (HCompose a1 b1 # h1)+        (a0 # HCompose b0 h0)+        (a1 # HCompose b1 h1) _HCompose = iso getHCompose HCompose  {-# ANN module "HLint: ignore Use camelCase" #-}@@ -48,9 +61,8 @@     {-# INLINE hLiftConstraint #-}     hLiftConstraint (HWitness (W_HCompose w0 w1)) p r =         hLiftConstraint w0 (p0 p) $-        withDict (hComposeConstraint0 p (Proxy @b) w0) $-        hLiftConstraint w1 (p1 p w0) $-        withDict (d0 p w0 w1) r+            hLiftConstraint w1 (p1 p w0) (withDict (d0 p w0 w1) r)+                \\ hComposeConstraint0 p (Proxy @b) w0         where             p0 :: Proxy c -> Proxy (HComposeConstraint0 c b)             p0 _ = Proxy@@ -58,12 +70,17 @@             p1 _ _ = Proxy             d0 ::                 HComposeConstraint1 c a0 b0 =>-                Proxy c -> HWitness a a0 -> HWitness b b0 -> Dict (c (HCompose a0 b0))+                Proxy c ->+                HWitness a a0 ->+                HWitness b b0 ->+                Dict (c (HCompose a0 b0))             d0 _ _ _ = hComposeConstraint1  class HComposeConstraint0 (c :: HyperType -> Constraint) (b :: HyperType) (h0 :: HyperType) where     hComposeConstraint0 ::-        proxy0 c -> proxy1 b -> proxy2 h0 ->+        proxy0 c ->+        proxy1 b ->+        proxy2 h0 ->         Dict (HNodesConstraint b (HComposeConstraint1 c h0))  instance HNodesConstraint b (HComposeConstraint1 c h0) => HComposeConstraint0 c b h0 where@@ -78,98 +95,110 @@     hComposeConstraint1 = Dict  instance-    (HNodes a, HPointed a, HPointed b) =>-    HPointed (HCompose a b) where+    (HPointed a, HPointed b) =>+    HPointed (HCompose a b)+    where     {-# INLINE hpure #-}     hpure x =-        _HCompose #-        hpure-        ( \wa ->-            _HCompose # hpure (\wb -> _HCompose # x (HWitness (W_HCompose wa wb)))-        )+        _HCompose+            # hpure+                ( \wa ->+                    _HCompose # hpure (\wb -> _HCompose # x (HWitness (W_HCompose wa wb)))+                )  instance (HFunctor a, HFunctor b) => HFunctor (HCompose a b) where     {-# INLINE hmap #-}     hmap f =-        _HCompose %~-        hmap-        ( \w0 ->-            _HCompose %~ hmap (\w1 -> _HCompose %~ f (HWitness (W_HCompose w0 w1)))-        )+        _HCompose+            %~ hmap+                ( \w0 ->+                    _HCompose %~ hmap (\w1 -> _HCompose %~ f (HWitness (W_HCompose w0 w1)))+                )  instance (HApply a, HApply b) => HApply (HCompose a b) where     {-# INLINE hzip #-}     hzip (HCompose a0) =-        _HCompose %~-        hmap-        ( \_ (HCompose b0 :*: HCompose b1) ->-            _HCompose #-            hmap-            ( \_ (HCompose i0 :*: HCompose i1) ->-                _HCompose # (i0 :*: i1)-            ) (hzip b0 b1)-        )-        . hzip a0+        _HCompose+            %~ hmap+                ( \_ (HCompose b0 :*: HCompose b1) ->+                    _HCompose+                        # hmap+                            ( \_ (HCompose i0 :*: HCompose i1) ->+                                _HCompose # (i0 :*: i1)+                            )+                            (hzip b0 b1)+                )+            . hzip a0  instance (HFoldable a, HFoldable b) => HFoldable (HCompose a b) where     {-# INLINE hfoldMap #-}     hfoldMap f =         hfoldMap-        ( \w0 ->-            hfoldMap (\w1 -> f (HWitness (W_HCompose w0 w1)) . (^. _HCompose)) . (^. _HCompose)-        ) . (^. _HCompose)+            ( \w0 ->+                hfoldMap (\w1 -> f (HWitness (W_HCompose w0 w1)) . (^. _HCompose)) . (^. _HCompose)+            )+            . (^. _HCompose)  instance (HTraversable a, HTraversable b) => HTraversable (HCompose a b) where     {-# INLINE hsequence #-}     hsequence =         _HCompose-        ( hsequence .-            hmap (const (MkContainedH . _HCompose (htraverse (const (_HCompose runContainedH)))))-        )+            ( hsequence+                . hmap (const (MkContainedH . _HCompose (htraverse (const (_HCompose runContainedH)))))+            )  instance     (ZipMatch h0, ZipMatch h1, HTraversable h0, HFunctor h1) =>-    ZipMatch (HCompose h0 h1) where+    ZipMatch (HCompose h0 h1)+    where     {-# INLINE zipMatch #-}     zipMatch (HCompose x) (HCompose y) =         zipMatch x y-        >>= htraverse-            (\_ (HCompose cx :*: HCompose cy) ->-                zipMatch cx cy-                <&> hmap-                    (\_ (HCompose bx :*: HCompose by) -> bx :*: by & HCompose)-                <&> (_HCompose #)-            )-        <&> (_HCompose #)+            >>= htraverse+                ( \_ (HCompose cx :*: HCompose cy) ->+                    zipMatch cx cy+                        <&> (_HCompose #) . hmap (\_ (HCompose bx :*: HCompose by) -> bx :*: by & HCompose)+                )+            <&> (_HCompose #)  instance-    ( HNodes a, HNodes b+    ( HNodes a+    , HNodes b     , HNodesConstraint a (HComposeConstraint0 RNodes b)-    ) => RNodes (HCompose a b)+    ) =>+    RNodes (HCompose a b)  instance-    ( HNodes h0, HNodes h1+    ( HNodes h0+    , HNodes h1     , c (HCompose h0 h1)     , HNodesConstraint h0 (HComposeConstraint0 RNodes h1)     , HNodesConstraint h0 (HComposeConstraint0 (Recursively c) h1)-    ) => Recursively c (HCompose h0 h1)+    ) =>+    Recursively c (HCompose h0 h1)  instance-    ( HTraversable a, HTraversable b+    ( HTraversable a+    , HTraversable b     , HNodesConstraint a (HComposeConstraint0 RNodes b)     , HNodesConstraint a (HComposeConstraint0 (Recursively HFunctor) b)     , HNodesConstraint a (HComposeConstraint0 (Recursively HFoldable) b)     , HNodesConstraint a (HComposeConstraint0 RTraversable b)-    ) => RTraversable (HCompose a b)+    ) =>+    RTraversable (HCompose a b)  hcomposed ::     (Profunctor p, Functor f) =>-    Optic p f+    Optic+        p+        f         (a0 # HCompose b0 c0)         (a1 # HCompose b1 c1)         (HCompose a2 b2 # c2)         (HCompose a3 b3 # c3) ->-    Optic p f+    Optic+        p+        f         (HCompose a0 b0 # c0)         (HCompose a1 b1 # c1)         (a2 # HCompose b2 c2)@@ -188,10 +217,12 @@     (Recursively HFunctor a, Recursively HFunctor b) =>     Iso' (Pure # HCompose a b) (a # b) decompose' =-    withDict (recursively (Proxy @(HFunctor a))) $-    withDict (recursively (Proxy @(HFunctor b))) $-    _Pure . _HCompose .-    hiso-    ( Proxy @(Recursively HFunctor) #>-        _HCompose . hiso (Proxy @(Recursively HFunctor) #> _HCompose . decompose')-    )+    _Pure+        . _HCompose+        . hiso+            ( Proxy @(Recursively HFunctor) #>+                _HCompose+                    . hiso (Proxy @(Recursively HFunctor) #> _HCompose . decompose')+                    \\ recursively (Proxy @(HFunctor b))+            )+        \\ recursively (Proxy @(HFunctor a))

@@ -1,17 +1,19 @@--- | A combinator to flip the order of the last two type parameters of a 'Hyper.Type.HyperType'.--{-# LANGUAGE TemplateHaskell, UndecidableInstances, FlexibleContexts #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE UndecidableInstances #-} +-- | A combinator to flip the order of the last two type parameters of a 'Hyper.Type.HyperType'. module Hyper.Combinator.Flip-    ( HFlip(..), _HFlip+    ( HFlip (..)+    , _HFlip     , hflipped     , htraverseFlipped     ) where -import Control.Lens (iso, from)+import Control.Lens (from, iso) import Hyper.Class.Nodes (HWitness) import Hyper.Class.Traversable (HTraversable, htraverse)-import Hyper.Type (type (#), GetHyperType)+import Hyper.Type (GetHyperType, type (#))  import Hyper.Internal.Prelude @@ -20,9 +22,9 @@ -- Useful to use instances of classes such as 'Hyper.Class.Traversable.HTraversable' which -- are available on the flipped 'Hyper.Type.HyperType'. -- For example 'Hyper.Unify.Generalize.GTerm' has instances when flipped.-newtype HFlip f x h =-    MkHFlip (f (GetHyperType h) # x)-    deriving stock Generic+newtype HFlip f x h+    = MkHFlip (f (GetHyperType h) # x)+    deriving stock (Generic)  makeCommonInstances [''HFlip] @@ -32,18 +34,18 @@ -- because it helps the type inference know that @ANode c@ is parameterized with a 'Hyper.Type.HyperType'. _HFlip ::     Iso-    (HFlip f0 x0 # k0)-    (HFlip f1 x1 # k1)-    (f0 k0 # x0)-    (f1 k1 # x1)+        (HFlip f0 x0 # k0)+        (HFlip f1 x1 # k1)+        (f0 k0 # x0)+        (f1 k1 # x1) _HFlip = iso (\(MkHFlip x) -> x) MkHFlip  hflipped ::     Iso-    (f0 k0 # x0)-    (f1 k1 # x1)-    (HFlip f0 x0 # k0)-    (HFlip f1 x1 # k1)+        (f0 k0 # x0)+        (f1 k1 # x1)+        (HFlip f0 x0 # k0)+        (HFlip f1 x1 # k1) hflipped = from _HFlip  -- | Convinience function for traversal over second last 'HyperType' argument.

@@ -1,5 +1,6 @@ module Hyper.Combinator.Func-    ( HFunc(..), _HFunc+    ( HFunc (..)+    , _HFunc     ) where  import Control.Lens (Iso, iso)@@ -8,7 +9,8 @@ newtype HFunc (i :: HyperType) o h = HFunc (i h -> o h)  _HFunc ::-    Iso (HFunc i0 o0 # h0)+    Iso+        (HFunc i0 o0 # h0)         (HFunc i1 o1 # h1)         (i0 # h0 -> o0 # h0)         (i1 # h1 -> o1 # h1)

@@ -1,18 +1,27 @@-{-# LANGUAGE TemplateHaskell, FlexibleContexts, UndecidableInstances #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE UndecidableInstances #-}  module Hyper.Diff     ( diff-    , Diff(..), _CommonBody, _CommonSubTree, _Different-    , CommonBody(..), anns, val+    , Diff (..)+    , _CommonBody+    , _CommonSubTree+    , _Different+    , CommonBody (..)+    , anns+    , val     , foldDiffs-     , diffP-    , DiffP(..), _CommonBodyP, _CommonSubTreeP, _DifferentP+    , DiffP (..)+    , _CommonBodyP+    , _CommonSubTreeP+    , _DifferentP     , foldDiffsP     ) where  import Hyper-import Hyper.Class.ZipMatch (ZipMatch(..))+import Hyper.Class.ZipMatch (ZipMatch (..)) import Hyper.Internal.Prelude import Hyper.Recurse @@ -23,14 +32,15 @@     = CommonSubTree (Ann (a :*: b) e)     | CommonBody (CommonBody a b e)     | Different ((Ann a :*: Ann b) e)-    deriving Generic+    deriving (Generic)  -- | A 'HyperType' which represents two trees which have the same top-level node, -- but their children may differ. data CommonBody a b e = MkCommonBody     { _anns :: (a :*: b) e     , _val :: e :# Diff a b-    } deriving Generic+    }+    deriving (Generic)  makePrisms ''Diff makeLenses ''CommonBody@@ -39,22 +49,26 @@ diff ::     forall t a b.     (Recursively ZipMatch t, RTraversable t) =>-    Ann a # t -> Ann b # t -> Diff a b # t+    Ann a # t ->+    Ann b # t ->+    Diff a b # t diff x@(Ann xA xB) y@(Ann yA yB) =-    withDict (recursively (Proxy @(ZipMatch t))) $-    withDict (recurse (Proxy @(RTraversable t))) $     case zipMatch xB yB of-    Nothing -> Different (x :*: y)-    Just match ->-        case htraverse (const (^? _CommonSubTree)) sub of-        Nothing -> MkCommonBody (xA :*: yA) sub & CommonBody-        Just r -> Ann (xA :*: yA) r & CommonSubTree-        where-            sub =-                hmap-                ( Proxy @(Recursively ZipMatch) #*# Proxy @RTraversable #>-                    \(xC :*: yC) -> diff xC yC-                ) match+        Nothing -> Different (x :*: y)+        Just match ->+            case htraverse (const (^? _CommonSubTree)) sub of+                Nothing -> MkCommonBody (xA :*: yA) sub & CommonBody+                Just r -> Ann (xA :*: yA) r & CommonSubTree+            where+                sub =+                    hmap+                        ( Proxy @(Recursively ZipMatch) #*#+                            Proxy @RTraversable #>+                                \(xC :*: yC) -> diff xC yC+                        )+                        match+                        \\ recurse (Proxy @(RTraversable t))+        \\ recursively (Proxy @(ZipMatch t))  foldDiffs ::     forall r h a b.@@ -65,49 +79,55 @@ foldDiffs _ CommonSubTree{} = mempty foldDiffs f (Different (x :*: y)) = f HRecSelf x y foldDiffs f (CommonBody (MkCommonBody _ x)) =-    withDict (recursively (Proxy @(HFoldable h))) $     hfoldMap-    ( Proxy @(Recursively HFoldable) #*#-        \w -> foldDiffs (f . HRecSub w)-    ) x+        ( Proxy @(Recursively HFoldable) #*#+            \w -> foldDiffs (f . HRecSub w)+        )+        x+        \\ recursively (Proxy @(HFoldable h))  data DiffP h     = CommonSubTreeP (HPlain (GetHyperType h))     | CommonBodyP (h :# DiffP)     | DifferentP (HPlain (GetHyperType h)) (HPlain (GetHyperType h))-    deriving Generic+    deriving (Generic) makePrisms ''DiffP  diffP ::     forall h.     (Recursively ZipMatch h, Recursively HasHPlain h, RTraversable h) =>-    HPlain h -> HPlain h -> DiffP # h+    HPlain h ->+    HPlain h ->+    DiffP # h diffP x y =-    withDict (recursively (Proxy @(HasHPlain h))) $     diffPH (x ^. hPlain) (y ^. hPlain)+        \\ recursively (Proxy @(HasHPlain h))  diffPH ::     forall h.     (Recursively ZipMatch h, Recursively HasHPlain h, RTraversable h) =>-    Pure # h -> Pure # h -> DiffP # h+    Pure # h ->+    Pure # h ->+    DiffP # h diffPH x y =-    withDict (recursively (Proxy @(ZipMatch h))) $-    withDict (recursively (Proxy @(HasHPlain h))) $-    withDict (recurse (Proxy @(RTraversable h))) $     case zipMatch (x ^. _Pure) (y ^. _Pure) of-    Nothing -> DifferentP (hPlain # x) (hPlain # y)-    Just match ->-        case htraverse_ (const ((() <$) . (^? _CommonSubTreeP))) sub of-        Nothing -> CommonBodyP sub-        Just () -> _CommonSubTreeP . hPlain # x-        where-            sub =-                hmap-                ( Proxy @(Recursively ZipMatch) #*#-                    Proxy @(Recursively HasHPlain) #*#-                    Proxy @RTraversable #>-                    \(xC :*: yC) -> diffPH xC yC-                ) match+        Nothing -> DifferentP (hPlain # x) (hPlain # y)+        Just match ->+            case htraverse_ (const ((() <$) . (^? _CommonSubTreeP))) sub of+                Nothing -> CommonBodyP sub+                Just () -> _CommonSubTreeP . hPlain # x+            where+                sub =+                    hmap+                        ( Proxy @(Recursively ZipMatch) #*#+                            Proxy @(Recursively HasHPlain) #*#+                                Proxy @RTraversable #>+                                    \(xC :*: yC) -> diffPH xC yC+                        )+                        match+                        \\ recurse (Proxy @(RTraversable h))+        \\ recursively (Proxy @(ZipMatch h))+        \\ recursively (Proxy @(HasHPlain h))  makeCommonInstances [''Diff, ''CommonBody, ''DiffP] @@ -118,13 +138,15 @@     DiffP # h ->     r foldDiffsP f =-    withDict (recursively (Proxy @(HasHPlain h))) $     \case-    CommonSubTreeP{} -> mempty-    DifferentP x y -> f HRecSelf x y-    CommonBodyP x ->-        withDict (recursively (Proxy @(HFoldable h))) $-        hfoldMap-        ( Proxy @(Recursively HFoldable) #*# Proxy @(Recursively HasHPlain) #*#-            \w -> foldDiffsP (f . HRecSub w)-        ) x+        CommonSubTreeP{} -> mempty+        DifferentP x y -> f HRecSelf x y+        CommonBodyP x ->+            hfoldMap+                ( Proxy @(Recursively HFoldable) #*#+                    Proxy @(Recursively HasHPlain) #*#+                        \w -> foldDiffsP (f . HRecSub w)+                )+                x+                \\ recursively (Proxy @(HFoldable h))+        \\ recursively (Proxy @(HasHPlain h))

@@ -2,31 +2,28 @@  module Hyper.Infer     ( infer-     , InferResultsConstraint     , inferUVarsApplyBindings-     , module Hyper.Class.Infer     , module Hyper.Class.Infer.Env     , module Hyper.Class.Infer.InferOf     , module Hyper.Infer.ScopeLevel     , module Hyper.Infer.Result--    , -- | Exported only for SPECIALIZE pragmas-      inferH+      -- | Exported only for SPECIALIZE pragmas+    , inferH     ) where  import qualified Control.Lens as Lens-import           Hyper-import           Hyper.Class.Infer-import           Hyper.Class.Infer.Env-import           Hyper.Class.Infer.InferOf-import           Hyper.Class.Nodes (HNodesHaveConstraint(..))-import           Hyper.Infer.Result-import           Hyper.Infer.ScopeLevel-import           Hyper.Unify (Unify, UVarOf, applyBindings)+import Hyper+import Hyper.Class.Infer+import Hyper.Class.Infer.Env+import Hyper.Class.Infer.InferOf+import Hyper.Class.Nodes (HNodesHaveConstraint (..))+import Hyper.Infer.Result+import Hyper.Infer.ScopeLevel+import Hyper.Unify (UVarOf, Unify, applyBindings) -import           Hyper.Internal.Prelude+import Hyper.Internal.Prelude  -- | Perform Hindley-Milner type inference of a term {-# INLINE infer #-}@@ -36,9 +33,9 @@     Ann a # t ->     m (Ann (a :*: InferResult (UVarOf m)) # t) infer (Ann a x) =-    withDict (inferContext (Proxy @m) (Proxy @t)) $     inferBody (hmap (Proxy @(Infer m) #> inferH) x)-    <&> (\(xI, t) -> Ann (a :*: InferResult t) xI)+        <&> (\(xI, t) -> Ann (a :*: InferResult t) xI)+        \\ inferContext (Proxy @m) (Proxy @t)  {-# INLINE inferH #-} inferH ::@@ -51,27 +48,30 @@  inferUVarsApplyBindings ::     forall m t a.-    ( Applicative m, RTraversable t, RTraversableInferOf t+    ( Applicative m+    , RTraversable t+    , Recursively (InferOfConstraint HTraversable) t     , InferResultsConstraint (Unify m) t     ) =>     Ann (a :*: InferResult (UVarOf m)) # t ->     m (Ann (a :*: InferResult (Pure :*: UVarOf m)) # t) inferUVarsApplyBindings =     htraverseFlipped $-    Proxy @RTraversableInferOf #*#-    Proxy @(InferResultsConstraint (Unify m)) #>-    Lens._2 f+        Proxy @(Recursively (InferOfConstraint HTraversable)) #*#+            Proxy @(InferResultsConstraint (Unify m)) #>+                Lens._2 f     where         f ::             forall n.-            ( HTraversable (InferOf n)+            ( Recursively (InferOfConstraint HTraversable) n             , InferResultsConstraint (Unify m) n             ) =>             InferResult (UVarOf m) # n ->             m (InferResult (Pure :*: UVarOf m) # n)-        f = withDict (recursively (Proxy @(InferOfConstraint (HNodesHaveConstraint (Unify m)) n))) $-            withDict (inferOfConstraint (Proxy @(HNodesHaveConstraint (Unify m))) (Proxy @n)) $-            withDict (hNodesHaveConstraint (Proxy @(Unify m)) (Proxy @(InferOf n))) $-            htraverseFlipped $-            Proxy @(Unify m) #>-            \x -> applyBindings x <&> (:*: x)+        f =+            htraverseFlipped (Proxy @(Unify m) #> \x -> applyBindings x <&> (:*: x))+                \\ inferOfConstraint @HTraversable (Proxy @n)+                \\ recursively (Proxy @(InferOfConstraint HTraversable n))+                \\ hNodesHaveConstraint (Proxy @(Unify m)) (Proxy @(InferOf n))+                \\ inferOfConstraint @(HNodesHaveConstraint (Unify m)) (Proxy @n)+                \\ recursively (Proxy @(InferOfConstraint (HNodesHaveConstraint (Unify m)) n))

@@ -1,3 +1,8 @@+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE UndecidableInstances #-}+ -- | Hindley-Milner type inference with ergonomic blame assignment. -- -- 'blame' is a type-error blame assignment algorithm for languages with Hindley-Milner type inference,@@ -31,29 +36,28 @@ -- -- Note: If a similar algorithm already existed somewhere, -- [I](https://github.com/yairchu/) would very much like to know!--{-# LANGUAGE FlexibleContexts, TemplateHaskell, FlexibleInstances, UndecidableInstances #-}- module Hyper.Infer.Blame     ( blame-    , Blame(..)-    , BlameResult(..), _Good, _Mismatch+    , Blame (..)+    , BlameResult (..)+    , _Good+    , _Mismatch     , InferOf'     ) where  import qualified Control.Lens as Lens-import           Control.Monad.Except (MonadError(..))-import           Data.List (sortOn)-import           Hyper-import           Hyper.Class.Infer-import           Hyper.Class.Traversable (ContainedH(..))-import           Hyper.Class.Unify (UnifyGen, UVarOf)-import           Hyper.Infer.Result-import           Hyper.Recurse-import           Hyper.Unify.New (newUnbound)-import           Hyper.Unify.Occurs (occursCheck)+import Control.Monad.Except (MonadError (..))+import Data.List (sortOn)+import Hyper+import Hyper.Class.Infer+import Hyper.Class.Traversable (ContainedH (..))+import Hyper.Class.Unify (UVarOf, UnifyGen)+import Hyper.Infer.Result+import Hyper.Recurse+import Hyper.Unify.New (newUnbound)+import Hyper.Unify.Occurs (occursCheck) -import           Hyper.Internal.Prelude+import Hyper.Internal.Prelude  -- | Class implementing some primitives needed by the 'blame' algorithm --@@ -61,8 +65,8 @@ -- It replaces context for 'Blame' to avoid @UndecidableSuperClasses@. class     (Infer m t, RTraversable t, HTraversable (InferOf t), HPointed (InferOf t)) =>-    Blame m t where-+    Blame m t+    where     -- | Unify the types/values in infer results     inferOfUnify ::         Proxy t ->@@ -78,12 +82,9 @@         m Bool      -- TODO: Putting documentation here causes duplication in the haddock documentation-    blamableRecursive ::-        Proxy m -> Proxy t -> Dict (HNodesConstraint t (Blame m))+    blamableRecursive :: Proxy m -> RecMethod (Blame m) t     {-# INLINE blamableRecursive #-}-    default blamableRecursive ::-        HNodesConstraint t (Blame m) =>-        Proxy m -> Proxy t -> Dict (HNodesConstraint t (Blame m))+    default blamableRecursive :: HNodesConstraint t (Blame m) => Proxy m -> RecMethod (Blame m) t     blamableRecursive _ _ = Dict  instance Recursive (Blame m) where@@ -98,10 +99,10 @@     Ann a # exp ->     m (Ann (a :*: InferResult (UVarOf m) :*: InferResult (UVarOf m)) # exp) prepareH t =-    withDict (inferContext (Proxy @m) (Proxy @exp)) $     hpure (Proxy @(UnifyGen m) #> MkContainedH newUnbound)-    & hsequence-    >>= (`prepare` t)+        & hsequence+        >>= (`prepare` t)+        \\ inferContext (Proxy @m) (Proxy @exp)  prepare ::     forall m exp a.@@ -110,15 +111,15 @@     Ann a # exp ->     m (Ann (a :*: InferResult (UVarOf m) :*: InferResult (UVarOf m)) # exp) prepare resFromPosition (Ann a x) =-    withDict (recurse (Proxy @(Blame m exp))) $     hmap-    ( Proxy @(Blame m) #>-        InferChild . fmap (\t -> InferredChild t (t ^. hAnn . Lens._2 . Lens._1 . _InferResult)) . prepareH-    ) x-    & inferBody-    <&>-    \(xI, r) ->-    Ann (a :*: InferResult resFromPosition :*: InferResult r) xI+        ( Proxy @(Blame m) #>+            InferChild . fmap (\t -> InferredChild t (t ^. hAnn . Lens._2 . Lens._1 . _InferResult)) . prepareH+        )+        x+        \\ recurse (Proxy @(Blame m exp))+        & inferBody+        <&> \(xI, r) ->+            Ann (a :*: InferResult resFromPosition :*: InferResult r) xI  tryUnify ::     forall err m top exp.@@ -128,16 +129,16 @@     InferOf exp # UVarOf m ->     m () tryUnify _ i0 i1 =-    withDict (inferContext (Proxy @m) (Proxy @exp)) $     do         inferOfUnify (Proxy @exp) i0 i1         htraverse_ (Proxy @(UnifyGen m) #> occursCheck) i0-    & (`catchError` const (pure ()))+            \\ inferContext (Proxy @m) (Proxy @exp)+        & (`catchError` const (pure ()))  data BlameResult v e     = Good (InferOf' e v)     | Mismatch (InferOf' e v, InferOf' e v)-    deriving Generic+    deriving (Generic) makePrisms ''BlameResult makeCommonInstances [''BlameResult] @@ -147,7 +148,6 @@     Ann (a :*: InferResult (UVarOf m) :*: InferResult (UVarOf m)) # exp ->     m (Ann (a :*: BlameResult (UVarOf m)) # exp) finalize (Ann (a :*: InferResult i0 :*: InferResult i1) x) =-    withDict (recurse (Proxy @(Blame m exp))) $     do         match <- inferOfMatches (Proxy @exp) i0 i1         let result@@ -155,6 +155,7 @@                 | otherwise = Mismatch (i0, i1)         htraverse (Proxy @(Blame m) #> finalize) x             <&> Ann (a :*: result)+        \\ recurse (Proxy @(Blame m exp))  -- | Perform Hindley-Milner type inference with prioritised blame for type error, -- given a prioritisation for the different nodes.@@ -183,7 +184,9 @@         hfoldMap             ( Proxy @(Blame m) #*#                 \w (a :*: InferResult i0 :*: InferResult i1) ->-                [(order a, tryUnify w i0 i1)]-            ) (_HFlip # p)-            & sortOn fst & traverse_ snd+                    [(order a, tryUnify w i0 i1)]+            )+            (_HFlip # p)+            & sortOn fst+            & traverse_ snd         finalize p

@@ -1,7 +1,11 @@-{-# LANGUAGE TemplateHaskell, UndecidableInstances, FlexibleInstances #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE UndecidableInstances #-}  module Hyper.Infer.Result-    ( InferResult(..), _InferResult+    ( InferResult (..)+    , _InferResult     , inferResult     ) where @@ -10,16 +14,18 @@ import Hyper.Internal.Prelude  -- | A 'HyperType' for an inferred term - the output of 'Hyper.Infer.infer'-newtype InferResult v e =-    InferResult (InferOf (GetHyperType e) # v)-    deriving stock Generic+newtype InferResult v e+    = InferResult (InferOf (GetHyperType e) # v)+    deriving stock (Generic)+ makePrisms ''InferResult makeCommonInstances [''InferResult]  -- An iso for the common case where the infer result of a term is a single value. inferResult ::     InferOf e ~ ANode t =>-    Iso (InferResult v0 # e)+    Iso+        (InferResult v0 # e)         (InferResult v1 # e)         (v0 # t)         (v1 # t)

@@ -1,16 +1,17 @@ {-# LANGUAGE TemplateHaskell #-}  module Hyper.Infer.ScopeLevel-    ( ScopeLevel(..), _ScopeLevel-    , MonadScopeLevel(..)+    ( ScopeLevel (..)+    , _ScopeLevel+    , MonadScopeLevel (..)     ) where -import           Algebra.PartialOrd (PartialOrd(..))-import           Hyper.Unify.Constraints (TypeConstraints(..))+import Algebra.PartialOrd (PartialOrd (..))+import Hyper.Unify.Constraints (TypeConstraints (..)) import qualified Text.PrettyPrint as Pretty-import           Text.PrettyPrint.HughesPJClass (Pretty(..))+import Text.PrettyPrint.HughesPJClass (Pretty (..)) -import           Hyper.Internal.Prelude+import Hyper.Internal.Prelude  -- | A representation of scope nesting level, -- for use in let-generalization and skolem escape detection.@@ -24,6 +25,7 @@ -- logical ordering, for which 'PartialOrd' is used. newtype ScopeLevel = ScopeLevel Int     deriving stock (Eq, Ord, Show, Generic)+ makePrisms ''ScopeLevel  instance PartialOrd ScopeLevel where

@@ -2,25 +2,24 @@  module Hyper.Internal.Prelude     ( makeCommonInstances-     , module X     ) where  import Control.DeepSeq as X (NFData)-import Control.Lens as X (Traversal, Iso, makeLenses, makePrisms)+import Control.Lens as X (Iso, Traversal, makeLenses, makePrisms) import Control.Lens.Operators as X-import Control.Monad as X (guard)+import Control.Monad as X (guard, void) import Data.Binary as X (Binary)-import Data.Constraint as X (Dict(..), Constraint, withDict)-import Data.Foldable as X (traverse_, sequenceA_)-import Data.Functor.Const as X (Const(..))-import Data.Proxy as X (Proxy(..))+import Data.Constraint as X (Constraint, Dict (..), (\\))+import Data.Foldable as X (sequenceA_, traverse_)+import Data.Functor.Const as X (Const (..)) import Data.Map as X (Map) import Data.Maybe as X (fromMaybe)+import Data.Proxy as X (Proxy (..)) import Data.Set as X (Set)+import GHC.Generics as X (Generic, (:*:) (..)) import Generics.Constraints (makeDerivings, makeInstances)-import GHC.Generics as X (Generic, (:*:)(..))-import Language.Haskell.TH (Name, DecsQ)+import Language.Haskell.TH (DecsQ, Name)  import Prelude.Compat as X @@ -28,5 +27,5 @@ makeCommonInstances :: [Name] -> DecsQ makeCommonInstances names =     (<>)-    <$> makeDerivings [''Eq, ''Ord, ''Show] names-    <*> makeInstances [''Binary, ''NFData] names+        <$> makeDerivings [''Eq, ''Ord, ''Show] names+        <*> makeInstances [''Binary, ''NFData] names

@@ -1,23 +1,28 @@--- | Combinators for processing/constructing trees recursively- {-# LANGUAGE FlexibleContexts #-} +-- | Combinators for processing/constructing trees recursively module Hyper.Recurse     ( module Hyper.Class.Recursive-    , fold, unfold-    , wrap, wrapM, unwrap, unwrapM+    , fold+    , unfold+    , wrap+    , wrapM+    , unwrap+    , unwrapM     , foldMapRecursive-    , HRecWitness(..)-    , (#>>), (#**#), (##>>)+    , HRecWitness (..)+    , (#>>)+    , (#**#)+    , (##>>)     ) where  import Hyper.Class.Foldable-import Hyper.Class.Functor (HFunctor(..))-import Hyper.Class.Nodes (HWitness, (#>), (#*#))+import Hyper.Class.Functor (HFunctor (..))+import Hyper.Class.Nodes (HWitness, (#*#), (#>)) import Hyper.Class.Recursive import Hyper.Class.Traversable import Hyper.Type-import Hyper.Type.Pure (Pure(..), _Pure)+import Hyper.Type.Pure (Pure (..), _Pure)  import Hyper.Internal.Prelude @@ -35,10 +40,10 @@     Pure # h ->     m (w # h) wrapM f x =-    withDict (recurse (Proxy @(RTraversable h))) $     x ^. _Pure-    & htraverse (Proxy @RTraversable #*# \w -> wrapM (f . HRecSub w))-    >>= f HRecSelf+        & htraverse (Proxy @RTraversable #*# \w -> wrapM (f . HRecSub w))+        >>= f HRecSelf+        \\ recurse (Proxy @(RTraversable h))  -- | Monadically unwrap a tree from the top down, replacing its 'HyperType' with 'Pure' {-# INLINE unwrapM #-}@@ -49,10 +54,10 @@     w # h ->     m (Pure # h) unwrapM f x =-    withDict (recurse (Proxy @(RTraversable h))) $     f HRecSelf x-    >>= htraverse (Proxy @RTraversable #*# \w -> unwrapM (f . HRecSub w))-    <&> (_Pure #)+        >>= htraverse (Proxy @RTraversable #*# \w -> unwrapM (f . HRecSub w))+        <&> (_Pure #)+        \\ recurse (Proxy @(RTraversable h))  -- | Wrap a 'Pure' to a different 'HyperType' from the bottom up {-# INLINE wrap #-}@@ -63,10 +68,10 @@     Pure # h ->     w # h wrap f x =-    withDict (recursively (Proxy @(HFunctor h))) $     x ^. _Pure-    & hmap (Proxy @(Recursively HFunctor) #*# \w -> wrap (f . HRecSub w))-    & f HRecSelf+        & hmap (Proxy @(Recursively HFunctor) #*# \w -> wrap (f . HRecSub w))+        & f HRecSelf+        \\ recursively (Proxy @(HFunctor h))  -- | Unwrap a tree from the top down, replacing its 'HyperType' with 'Pure' {-# INLINE unwrap #-}@@ -77,10 +82,11 @@     w # h ->     Pure # h unwrap f x =-    withDict (recursively (Proxy @(HFunctor h))) $-    _Pure #-    hmap (Proxy @(Recursively HFunctor) #*# \w -> unwrap (f . HRecSub w))-    (f HRecSelf x)+    _Pure+        # hmap+            (Proxy @(Recursively HFunctor) #*# \w -> unwrap (f . HRecSub w))+            (f HRecSelf x)+        \\ recursively (Proxy @(HFunctor h))  -- | Recursively fold up a tree to produce a result (aka catamorphism) {-# INLINE fold #-}@@ -109,13 +115,15 @@     h # p ->     a foldMapRecursive f x =-    withDict (recursively (Proxy @(HFoldable h))) $-    withDict (recursively (Proxy @(HFoldable p))) $-    f HRecSelf x <>-    hfoldMap-    ( Proxy @(Recursively HFoldable) #*#-        \w -> hfoldMap (Proxy @(Recursively HFoldable) #> foldMapRecursive (f . HRecSub w))-    ) x+    f HRecSelf x+        <> hfoldMap+            ( Proxy @(Recursively HFoldable) #*#+                \w ->+                    hfoldMap (Proxy @(Recursively HFoldable) #> foldMapRecursive (f . HRecSub w))+                        \\ recursively (Proxy @(HFoldable p))+            )+            x+        \\ recursively (Proxy @(HFoldable h))  infixr 0 #>> infixr 0 ##>>@@ -126,24 +134,30 @@ (#>>) ::     forall c h n r.     (Recursive c, c h, RNodes h) =>-    Proxy c -> (c n => r) -> HRecWitness h n -> r+    Proxy c ->+    (c n => r) ->+    HRecWitness h n ->+    r (#>>) _ r HRecSelf = r (#>>) p r (HRecSub w0 w1) =-    withDict (recurse (Proxy @(RNodes h))) $-    withDict (recurse (Proxy @(c h))) $     (Proxy @RNodes #*# p #> (p #>> r) w1) w0+        \\ recurse (Proxy @(RNodes h))+        \\ recurse (Proxy @(c h))  -- | @Proxy @c #> r@ replaces a recursive witness parameter of @r@ with a @Recursively c@ constraint on the witnessed node {-# INLINE (##>>) #-} (##>>) ::     forall c h n r.     Recursively c h =>-    Proxy c -> (c n => r) -> HRecWitness h n -> r+    Proxy c ->+    (c n => r) ->+    HRecWitness h n ->+    r (##>>) p r =-    withDict (recursively (Proxy @(c h))) $     \case-    HRecSelf -> r-    HRecSub w0 w1 -> (Proxy @(Recursively c) #> (p ##>> r) w1) w0+        HRecSelf -> r+        HRecSub w0 w1 -> (Proxy @(Recursively c) #> (p ##>> r) w1) w0+        \\ recursively (Proxy @(c h))  -- | A variant of '#>>' which does not consume the witness parameter. --@@ -151,5 +165,8 @@ {-# INLINE (#**#) #-} (#**#) ::     (Recursive c, c h, RNodes h) =>-    Proxy c -> (c n => HRecWitness h n -> r) -> HRecWitness h n -> r+    Proxy c ->+    (c n => HRecWitness h n -> r) ->+    HRecWitness h n ->+    r (#**#) p r w = (p #>> r) w w

@@ -0,0 +1,12 @@+-- | Common programming language syntax ingredients+module Hyper.Syntax+    ( module X+    ) where++import Hyper.Syntax.App as X+import Hyper.Syntax.FuncType as X+import Hyper.Syntax.Lam as X+import Hyper.Syntax.Let as X+import Hyper.Syntax.TypeSig as X+import Hyper.Syntax.TypedLam as X+import Hyper.Syntax.Var as X

@@ -0,0 +1,72 @@+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE UndecidableInstances #-}++module Hyper.Syntax.App+    ( App (..)+    , appFunc+    , appArg+    , W_App (..)+    , MorphWitness (..)+    ) where++import Hyper+import Hyper.Class.Optic (HSubset (..), HSubset')+import Hyper.Infer+import Hyper.Syntax.FuncType+import Hyper.Unify (UnifyGen, unify)+import Hyper.Unify.New (newTerm, newUnbound)+import Text.PrettyPrint ((<+>))+import Text.PrettyPrint.HughesPJClass (Pretty (..), maybeParens)++import Hyper.Internal.Prelude++-- | A term for function applications.+--+-- @App expr@s express function applications of @expr@s.+--+-- Apart from the data type, an 'Infer' instance is also provided.+data App expr h = App+    { _appFunc :: h :# expr+    , _appArg :: h :# expr+    }+    deriving (Generic)++makeLenses ''App+makeZipMatch ''App+makeHContext ''App+makeHMorph ''App+makeHTraversableApplyAndBases ''App+makeCommonInstances [''App]++instance RNodes e => RNodes (App e)+instance (c (App e), Recursively c e) => Recursively c (App e)+instance RTraversable e => RTraversable (App e)++instance Pretty (h :# expr) => Pretty (App expr h) where+    pPrintPrec lvl p (App f x) =+        pPrintPrec lvl 10 f+            <+> pPrintPrec lvl 11 x+            & maybeParens (p > 10)++type instance InferOf (App e) = ANode (TypeOf e)++instance+    ( Infer m expr+    , HasInferredType expr+    , HSubset' (TypeOf expr) (FuncType (TypeOf expr))+    , UnifyGen m (TypeOf expr)+    ) =>+    Infer m (App expr)+    where+    {-# INLINE inferBody #-}+    inferBody (App func arg) =+        do+            InferredChild argI argR <- inferChild arg+            InferredChild funcI funcR <- inferChild func+            funcRes <- newUnbound+            (App funcI argI, MkANode funcRes)+                <$ (newTerm (hSubset # FuncType (argR ^# l) funcRes) >>= unify (funcR ^# l))+        where+            l = inferredType (Proxy @expr)

@@ -0,0 +1,45 @@+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE UndecidableInstances #-}++module Hyper.Syntax.FuncType+    ( FuncType (..)+    , funcIn+    , funcOut+    , W_FuncType (..)+    , MorphWitness (..)+    ) where++import Generics.Constraints (makeDerivings, makeInstances)+import Hyper+import Text.PrettyPrint ((<+>))+import qualified Text.PrettyPrint as Pretty+import Text.PrettyPrint.HughesPJClass (Pretty (..), maybeParens)+import Text.Show.Combinators (showCon, (@|))++import Hyper.Internal.Prelude++-- | A term for the types of functions. Analogues to @(->)@ in Haskell.+--+-- @FuncType typ@s express types of functions of @typ@.+data FuncType typ h = FuncType+    { _funcIn :: h :# typ+    , _funcOut :: h :# typ+    }+    deriving (Generic)++makeLenses ''FuncType+makeZipMatch ''FuncType+makeHContext ''FuncType+makeHMorph ''FuncType+makeHTraversableApplyAndBases ''FuncType+makeDerivings [''Eq, ''Ord] [''FuncType]+makeInstances [''Binary, ''NFData] [''FuncType]++instance Pretty (h :# typ) => Pretty (FuncType typ h) where+    pPrintPrec lvl p (FuncType i o) =+        pPrintPrec lvl 11 i <+> Pretty.text "->" <+> pPrintPrec lvl 10 o+            & maybeParens (p > 10)++instance Show (h :# typ) => Show (FuncType typ h) where+    showsPrec p (FuncType i o) = (showCon "FuncType" @| i @| o) p

@@ -0,0 +1,76 @@+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE UndecidableInstances #-}++module Hyper.Syntax.Lam+    ( Lam (..)+    , lamIn+    , lamOut+    , W_Lam (..)+    , MorphWitness (..)+    ) where++import Generics.Constraints (Constraints)+import Hyper+import Hyper.Class.Optic (HSubset (..), HSubset')+import Hyper.Infer+import Hyper.Syntax.FuncType+import Hyper.Unify (UVarOf, UnifyGen)+import Hyper.Unify.New (newTerm, newUnbound)+import qualified Text.PrettyPrint as P+import Text.PrettyPrint.HughesPJClass (Pretty (..), maybeParens)++import Hyper.Internal.Prelude++-- | A term for lambda abstractions.+--+-- @Lam v expr@s express lambda abstractions with @v@s as variable names and @expr@s for bodies.+--+-- Apart from the data type, an 'Infer' instance is also provided.+data Lam v expr h = Lam+    { _lamIn :: v+    , _lamOut :: h :# expr+    }+    deriving (Generic)++makeLenses ''Lam+makeCommonInstances [''Lam]+makeHTraversableApplyAndBases ''Lam+makeZipMatch ''Lam+makeHContext ''Lam+makeHMorph ''Lam++instance RNodes t => RNodes (Lam v t)+instance (c (Lam v t), Recursively c t) => Recursively c (Lam v t)+instance RTraversable t => RTraversable (Lam v t)++instance+    Constraints (Lam v expr h) Pretty =>+    Pretty (Lam v expr h)+    where+    pPrintPrec lvl p (Lam i o) =+        (P.text "λ" <> pPrintPrec lvl 0 i)+            P.<+> P.text "→"+            P.<+> pPrintPrec lvl 0 o+            & maybeParens (p > 0)++type instance InferOf (Lam _ t) = ANode (TypeOf t)++instance+    ( Infer m t+    , UnifyGen m (TypeOf t)+    , HSubset' (TypeOf t) (FuncType (TypeOf t))+    , HasInferredType t+    , LocalScopeType v (UVarOf m # TypeOf t) m+    ) =>+    Infer m (Lam v t)+    where+    {-# INLINE inferBody #-}+    inferBody (Lam p r) =+        do+            varType <- newUnbound+            InferredChild rI rR <- inferChild r & localScopeType p varType+            hSubset # FuncType varType (rR ^# inferredType (Proxy @t))+                & newTerm+                <&> (Lam p rI,) . MkANode

@@ -0,0 +1,80 @@+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE UndecidableInstances #-}++module Hyper.Syntax.Let+    ( Let (..)+    , letVar+    , letEquals+    , letIn+    , W_Let (..)+    , MorphWitness (..)+    ) where++import Generics.Constraints (Constraints)+import Hyper+import Hyper.Class.Unify (UVarOf, UnifyGen)+import Hyper.Infer+import Hyper.Unify.Generalize (GTerm, generalize)+import Text.PrettyPrint (($+$), (<+>))+import qualified Text.PrettyPrint as Pretty+import Text.PrettyPrint.HughesPJClass (Pretty (..), maybeParens)++import Hyper.Internal.Prelude++-- | A term for let-expressions with let-generalization.+--+-- @Let v expr@s express let-expressions with @v@s as variable names and @expr@s for terms.+--+-- Apart from the data type, an 'Infer' instance is also provided.+data Let v expr h = Let+    { _letVar :: v+    , _letEquals :: h :# expr+    , _letIn :: h :# expr+    }+    deriving (Generic)++makeLenses ''Let+makeCommonInstances [''Let]+makeHTraversableApplyAndBases ''Let+makeZipMatch ''Let+makeHContext ''Let+makeHMorph ''Let++instance+    Constraints (Let v expr h) Pretty =>+    Pretty (Let v expr h)+    where+    pPrintPrec lvl p (Let v e i) =+        Pretty.text "let"+            <+> pPrintPrec lvl 0 v+            <+> Pretty.text "="+            <+> pPrintPrec lvl 0 e+            $+$ pPrintPrec lvl 0 i+            & maybeParens (p > 0)++type instance InferOf (Let _ e) = InferOf e++instance+    ( MonadScopeLevel m+    , LocalScopeType v (GTerm (UVarOf m) # TypeOf expr) m+    , UnifyGen m (TypeOf expr)+    , HasInferredType expr+    , HNodesConstraint (InferOf expr) (UnifyGen m)+    , HTraversable (InferOf expr)+    , Infer m expr+    ) =>+    Infer m (Let v expr)+    where+    inferBody (Let v e i) =+        do+            (eI, eG) <-+                do+                    InferredChild eI eR <- inferChild e+                    generalize (eR ^# inferredType (Proxy @expr))+                        <&> (eI,)+                    & localLevel+            inferChild i+                & localScopeType v eG+                <&> \(InferredChild iI iR) -> (Let v eI iI, iR)

@@ -0,0 +1,45 @@+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE UndecidableInstances #-}++module Hyper.Syntax.Map+    ( TermMap (..)+    , _TermMap+    , W_TermMap (..)+    , MorphWitness (..)+    ) where++import qualified Control.Lens as Lens+import qualified Data.Map as Map+import Hyper+import Hyper.Class.ZipMatch (ZipMatch (..))++import Hyper.Internal.Prelude++-- | A mapping of keys to terms.+--+-- Apart from the data type, a 'ZipMatch' instance is also provided.+newtype TermMap h expr f = TermMap (Map h (f :# expr))+    deriving stock (Generic)++makePrisms ''TermMap+makeCommonInstances [''TermMap]+makeHTraversableApplyAndBases ''TermMap+makeHMorph ''TermMap++instance Eq h => ZipMatch (TermMap h expr) where+    {-# INLINE zipMatch #-}+    zipMatch (TermMap x) (TermMap y)+        | Map.size x /= Map.size y = Nothing+        | otherwise =+            zipMatchList (x ^@.. Lens.itraversed) (y ^@.. Lens.itraversed)+                <&> TermMap . Map.fromAscList . (traverse . Lens._2 %~ uncurry (:*:))++{-# INLINE zipMatchList #-}+zipMatchList :: Eq k => [(k, a)] -> [(k, b)] -> Maybe [(k, (a, b))]+zipMatchList [] [] = Just []+zipMatchList ((k0, v0) : xs) ((k1, v1) : ys)+    | k0 == k1 =+        zipMatchList xs ys <&> ((k0, (v0, v1)) :)+zipMatchList _ _ = Nothing

@@ -0,0 +1,398 @@+{-# LANGUAGE EmptyCase #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE UndecidableInstances #-}++-- | Nominal (named) types declaration, instantiation, construction, and access.+module Hyper.Syntax.Nominal+    ( NominalDecl (..)+    , nParams+    , nScheme+    , W_NominalDecl (..)+    , NominalInst (..)+    , nId+    , nArgs+    , ToNom (..)+    , tnId+    , tnVal+    , W_ToNom (..)+    , FromNom (..)+    , _FromNom+    , HasNominalInst (..)+    , NomVarTypes+    , MonadNominals (..)+    , LoadedNominalDecl+    , loadNominalDecl+    ) where++import Control.Applicative (Alternative (..))+import Control.Lens (Prism')+import qualified Control.Lens as Lens+import Control.Monad.Writer (WriterT (..), execWriterT)+import Generics.Constraints (Constraints)+import Hyper+import Hyper.Class.Context (HContext (..))+import Hyper.Class.Optic+import Hyper.Class.Traversable (ContainedH (..))+import Hyper.Class.ZipMatch (ZipMatch (..))+import Hyper.Infer+import Hyper.Recurse+import Hyper.Syntax.FuncType (FuncType (..))+import Hyper.Syntax.Map (TermMap (..), _TermMap)+import Hyper.Syntax.Scheme+import Hyper.Unify+import Hyper.Unify.Generalize (GTerm (..), instantiate, instantiateForAll, instantiateWith, _GMono)+import Hyper.Unify.New (newTerm)+import Hyper.Unify.QuantifiedVar (HasQuantifiedVar (..), OrdQVar)+import Hyper.Unify.Term (UTerm (..))+import qualified Text.PrettyPrint as P+import Text.PrettyPrint.HughesPJClass (Pretty (..), maybeParens)++import Hyper.Internal.Prelude++type family NomVarTypes (t :: HyperType) :: HyperType++-- | A declaration of a nominal type.+data NominalDecl typ h = NominalDecl+    { _nParams :: NomVarTypes typ # QVars+    , _nScheme :: Scheme (NomVarTypes typ) typ h+    }+    deriving (Generic)++-- | An instantiation of a nominal type+data NominalInst nomId varTypes h = NominalInst+    { _nId :: nomId+    , _nArgs :: varTypes # QVarInstances (GetHyperType h)+    }+    deriving (Generic)++-- | Nominal data constructor.+--+-- Wrap content with a data constructor+-- (analogues to a data constructor of a Haskell `newtype`'s).+--+-- Introduces the nominal's foralled type variables into the value's scope.+data ToNom nomId term h = ToNom+    { _tnId :: nomId+    , _tnVal :: h :# term+    }+    deriving (Generic)++-- | Access the data in a nominally typed value.+--+-- Analogues to a getter of a Haskell `newtype`.+newtype FromNom nomId (term :: HyperType) (h :: AHyperType) = FromNom nomId+    deriving newtype (Eq, Ord, Binary, NFData)+    deriving stock (Show, Generic)++-- | A nominal declaration loaded into scope in an inference monad.+data LoadedNominalDecl typ v = LoadedNominalDecl+    { lnParams :: NomVarTypes typ # QVarInstances (GetHyperType v)+    , lnForalls :: NomVarTypes typ # QVarInstances (GetHyperType v)+    , lnType :: GTerm (GetHyperType v) # typ+    }+    deriving (Generic)++makeLenses ''NominalDecl+makeLenses ''NominalInst+makeLenses ''ToNom+makePrisms ''FromNom+makeCommonInstances [''NominalDecl, ''NominalInst, ''ToNom, ''LoadedNominalDecl]+makeHTraversableAndBases ''NominalDecl+makeHTraversableApplyAndBases ''ToNom+makeHTraversableApplyAndBases ''FromNom+makeHMorph ''ToNom+makeZipMatch ''ToNom+makeZipMatch ''FromNom+makeHContext ''ToNom+makeHContext ''FromNom++instance HNodes v => HNodes (NominalInst n v) where+    type HNodesConstraint (NominalInst n v) c = HNodesConstraint v c+    type HWitnessType (NominalInst n v) = HWitnessType v+    {-# INLINE hLiftConstraint #-}+    hLiftConstraint (HWitness w) = hLiftConstraint @v (HWitness w)++instance HFunctor v => HFunctor (NominalInst n v) where+    {-# INLINE hmap #-}+    hmap f = nArgs %~ hmap (\(HWitness w) -> _QVarInstances . Lens.mapped %~ f (HWitness w))++instance HFoldable v => HFoldable (NominalInst n v) where+    {-# INLINE hfoldMap #-}+    hfoldMap f =+        hfoldMap (\(HWitness w) -> foldMap (f (HWitness w)) . (^. _QVarInstances)) . (^. nArgs)++instance HTraversable v => HTraversable (NominalInst n v) where+    {-# INLINE hsequence #-}+    hsequence (NominalInst n v) =+        htraverse (const (_QVarInstances (traverse runContainedH))) v+            <&> NominalInst n++instance+    ( Eq nomId+    , ZipMatch varTypes+    , HTraversable varTypes+    , HNodesConstraint varTypes ZipMatch+    , HNodesConstraint varTypes OrdQVar+    ) =>+    ZipMatch (NominalInst nomId varTypes)+    where+    {-# INLINE zipMatch #-}+    zipMatch (NominalInst xId x) (NominalInst yId y)+        | xId /= yId = Nothing+        | otherwise =+            zipMatch x y+                >>= htraverse+                    ( Proxy @ZipMatch #*#+                        Proxy @OrdQVar #>+                            \(QVarInstances c0 :*: QVarInstances c1) ->+                                zipMatch (TermMap c0) (TermMap c1)+                                    <&> QVarInstances . (^. _TermMap)+                    )+                <&> NominalInst xId++instance+    ( HFunctor varTypes+    , HContext varTypes+    , HNodesConstraint varTypes OrdQVar+    ) =>+    HContext (NominalInst nomId varTypes)+    where+    hcontext (NominalInst n args) =+        hcontext args+            & hmap+                ( Proxy @OrdQVar #>+                    \(HFunc c :*: x) ->+                        x+                            & _QVarInstances+                                . Lens.imapped+                                %@~ \k v ->+                                    HFunc+                                        ( \newV ->+                                            x+                                                & _QVarInstances . Lens.at k ?~ newV+                                                & c+                                                & getConst+                                                & NominalInst n+                                                & Const+                                        )+                                        :*: v+                )+            & NominalInst n++instance Constraints (ToNom nomId term h) Pretty => Pretty (ToNom nomId term h) where+    pPrintPrec lvl p (ToNom nomId term) =+        (pPrint nomId <> P.text "#") P.<+> pPrintPrec lvl 11 term+            & maybeParens (p > 10)++class (Pretty (QVar h), Pretty (outer :# h)) => PrettyConstraints outer h+instance (Pretty (QVar h), Pretty (outer :# h)) => PrettyConstraints outer h++instance+    ( Pretty nomId+    , HApply varTypes+    , HFoldable varTypes+    , HNodesConstraint varTypes (PrettyConstraints h)+    ) =>+    Pretty (NominalInst nomId varTypes h)+    where+    pPrint (NominalInst n vars) =+        pPrint n+            <> joinArgs+                (hfoldMap (Proxy @(PrettyConstraints h) #> mkArgs) vars)+        where+            joinArgs [] = mempty+            joinArgs xs = P.text "[" <> P.sep (P.punctuate (P.text ",") xs) <> P.text "]"+            mkArgs (QVarInstances m) =+                m ^@.. Lens.itraversed+                    <&> \(h, v) ->+                        (pPrint h <> P.text ":") P.<+> pPrint v++{-# ANN module "HLint: ignore Use camelCase" #-}+data W_LoadedNominalDecl t n where+    E_LoadedNominalDecl_Body :: HRecWitness t n -> W_LoadedNominalDecl t n+    E_LoadedNominalDecl_NomVarTypes :: HWitness (NomVarTypes t) n -> W_LoadedNominalDecl t n++instance (RNodes t, HNodes (NomVarTypes t)) => HNodes (LoadedNominalDecl t) where+    type+        HNodesConstraint (LoadedNominalDecl t) c =+            ( HNodesConstraint (NomVarTypes t) c+            , c t+            , Recursive c+            )+    type HWitnessType (LoadedNominalDecl t) = W_LoadedNominalDecl t+    {-# INLINE hLiftConstraint #-}+    hLiftConstraint (HWitness (E_LoadedNominalDecl_Body w)) = hLiftConstraint @(HFlip GTerm _) (HWitness w)+    hLiftConstraint (HWitness (E_LoadedNominalDecl_NomVarTypes w)) = hLiftConstraint w++instance+    (Recursively HFunctor typ, HFunctor (NomVarTypes typ)) =>+    HFunctor (LoadedNominalDecl typ)+    where+    {-# INLINE hmap #-}+    hmap f (LoadedNominalDecl mp mf t) =+        LoadedNominalDecl+            (onMap mp)+            (onMap mf)+            (t & hflipped %~ hmap (\(HWitness w) -> f (HWitness (E_LoadedNominalDecl_Body w))))+        where+            onMap = hmap (\w -> _QVarInstances . Lens.mapped %~ f (HWitness (E_LoadedNominalDecl_NomVarTypes w)))++instance+    (Recursively HFoldable typ, HFoldable (NomVarTypes typ)) =>+    HFoldable (LoadedNominalDecl typ)+    where+    {-# INLINE hfoldMap #-}+    hfoldMap f (LoadedNominalDecl mp mf t) =+        onMap mp+            <> onMap mf+            <> hfoldMap (\(HWitness w) -> f (HWitness (E_LoadedNominalDecl_Body w))) (_HFlip # t)+        where+            onMap =+                hfoldMap+                    ( \w ->+                        foldMap (f (HWitness (E_LoadedNominalDecl_NomVarTypes w)))+                            . (^. _QVarInstances)+                    )++instance+    (RTraversable typ, HTraversable (NomVarTypes typ)) =>+    HTraversable (LoadedNominalDecl typ)+    where+    {-# INLINE hsequence #-}+    hsequence (LoadedNominalDecl p f t) =+        LoadedNominalDecl+            <$> onMap p+            <*> onMap f+            <*> hflipped hsequence t+        where+            onMap = htraverse (const ((_QVarInstances . traverse) runContainedH))++{-# INLINE loadBody #-}+loadBody ::+    ( UnifyGen m typ+    , HNodeLens varTypes typ+    , Ord (QVar typ)+    ) =>+    varTypes # QVarInstances (UVarOf m) ->+    varTypes # QVarInstances (UVarOf m) ->+    typ # GTerm (UVarOf m) ->+    m (GTerm (UVarOf m) # typ)+loadBody params foralls x =+    case x ^? quantifiedVar >>= get of+        Just r -> GPoly r & pure+        Nothing ->+            case htraverse (const (^? _GMono)) x of+                Just xm -> newTerm xm <&> GMono+                Nothing -> GBody x & pure+    where+        get v =+            params ^? hNodeLens . _QVarInstances . Lens.ix v+                <|> foralls ^? hNodeLens . _QVarInstances . Lens.ix v++{-# INLINE loadNominalDecl #-}+loadNominalDecl ::+    forall m typ.+    ( HTraversable (NomVarTypes typ)+    , HNodesConstraint (NomVarTypes typ) (Unify m)+    , HasScheme (NomVarTypes typ) m typ+    ) =>+    Pure # NominalDecl typ ->+    m (LoadedNominalDecl typ # UVarOf m)+loadNominalDecl (Pure (NominalDecl params (Scheme foralls typ))) =+    do+        paramsL <- htraverse (Proxy @(Unify m) #> makeQVarInstances) params+        forallsL <- htraverse (Proxy @(Unify m) #> makeQVarInstances) foralls+        wrapM+            ( Proxy @(HasScheme (NomVarTypes typ) m) #>>+                loadBody paramsL forallsL+            )+            typ+            <&> LoadedNominalDecl paramsL forallsL++class MonadNominals nomId typ m where+    getNominalDecl :: nomId -> m (LoadedNominalDecl typ # UVarOf m)++class HasNominalInst nomId typ where+    nominalInst :: Prism' (typ # h) (NominalInst nomId (NomVarTypes typ) # h)++type instance InferOf (ToNom n e) = NominalInst n (NomVarTypes (TypeOf e))++instance+    ( MonadScopeLevel m+    , MonadNominals nomId (TypeOf expr) m+    , HTraversable (NomVarTypes (TypeOf expr))+    , HNodesConstraint (NomVarTypes (TypeOf expr)) (UnifyGen m)+    , UnifyGen m (TypeOf expr)+    , HasInferredType expr+    , Infer m expr+    ) =>+    Infer m (ToNom nomId expr)+    where+    {-# INLINE inferBody #-}+    inferBody (ToNom nomId val) =+        do+            LoadedNominalDecl params foralls gen <- getNominalDecl nomId++            -- Setup forall variables to instantiate to skolems.+            -- This means they aren't allow to be be unified,+            -- nor to propagate to outer scope.+            recoverForAlls <-+                htraverse_+                    ( Proxy @(UnifyGen m) #>+                        traverse_ (instantiateForAll USkolem) . (^. _QVarInstances)+                    )+                    foralls+                    & localLevel . execWriterT+            -- Setup params in outer scope+            (paramsT, recoverParams) <-+                htraverse+                    ( Proxy @(UnifyGen m) #>+                        (_QVarInstances . traverse) (instantiateForAll UUnbound)+                    )+                    params+                    & runWriterT++            typ <- instantiate gen & localLevel++            -- Restore loaded nominal to original reusable state+            sequence_ (recoverParams <> recoverForAlls)++            -- Term within is in inner level+            InferredChild valI valR <- inferChild val & localLevel++            -- Unify the inner term's type with the type inside the nominal+            _ <- unify typ (valR ^# inferredType (Proxy @expr))+            pure (ToNom nomId valI, NominalInst nomId paramsT)++type instance InferOf (FromNom _ e) = FuncType (TypeOf e)++instance+    ( Infer m expr+    , HasNominalInst nomId (TypeOf expr)+    , MonadNominals nomId (TypeOf expr) m+    , HTraversable (NomVarTypes (TypeOf expr))+    , HNodesConstraint (NomVarTypes (TypeOf expr)) (UnifyGen m)+    , UnifyGen m (TypeOf expr)+    ) =>+    Infer m (FromNom nomId expr)+    where+    {-# INLINE inferBody #-}+    inferBody (FromNom nomId) =+        do+            (LoadedNominalDecl params _ gen) <- getNominalDecl nomId+            let lookupParams = htraverse (Proxy @(UnifyGen m) #> (_QVarInstances . traverse) lookupParam) params+            (typ, paramsT) <- instantiateWith lookupParams UUnbound gen+            newTerm (nominalInst # NominalInst nomId paramsT)+                <&> (FromNom nomId,) . (`FuncType` typ)++lookupParam :: forall m t. UnifyGen m t => UVarOf m # t -> m (UVarOf m # t)+lookupParam v =+    lookupVar binding v+        >>= \case+            UInstantiated r -> pure r+            USkolem l ->+                -- This is a phantom-type, wasn't instantiated by `instantiate`.+                scopeConstraints (Proxy @t) <&> (<> l) >>= newVar binding . UUnbound+            _ -> error "unexpected state at nominal's parameter"

@@ -0,0 +1,184 @@+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE UndecidableInstances #-}++-- | Row types+module Hyper.Syntax.Row+    ( RowConstraints (..)+    , RowKey+    , RowExtend (..)+    , eKey+    , eVal+    , eRest+    , W_RowExtend (..)+    , FlatRowExtends (..)+    , freExtends+    , freRest+    , W_FlatRowExtends (..)+    , MorphWitness (..)+    , flattenRow+    , flattenRowExtend+    , unflattenRow+    , verifyRowExtendConstraints+    , rowExtendStructureMismatch+    , rowElementInfer+    ) where++import Control.Lens (Lens', Prism', contains)+import qualified Control.Lens as Lens+import Control.Monad (foldM)+import qualified Data.Map as Map+import Generics.Constraints (Constraints, makeDerivings, makeInstances)+import Hyper+import Hyper.Unify+import Hyper.Unify.New (newTerm, newUnbound)+import Hyper.Unify.Term (UTerm (..), UTermBody (..), uBody, _UTerm)+import Text.Show.Combinators (showCon, (@|))++import Hyper.Internal.Prelude++class+    (Ord (RowConstraintsKey constraints), TypeConstraints constraints) =>+    RowConstraints constraints+    where+    type RowConstraintsKey constraints+    forbidden :: Lens' constraints (Set (RowConstraintsKey constraints))++type RowKey typ = RowConstraintsKey (TypeConstraintsOf typ)++-- | Row-extend primitive for use in both value-level and type-level+data RowExtend key val rest h = RowExtend+    { _eKey :: key+    , _eVal :: h :# val+    , _eRest :: h :# rest+    }+    deriving (Generic)++data FlatRowExtends key val rest h = FlatRowExtends+    { _freExtends :: Map key (h :# val)+    , _freRest :: h :# rest+    }+    deriving (Generic)++makeLenses ''RowExtend+makeLenses ''FlatRowExtends+makeCommonInstances [''FlatRowExtends]+makeZipMatch ''RowExtend+makeHContext ''RowExtend+makeHMorph ''RowExtend+makeHTraversableApplyAndBases ''RowExtend+makeHTraversableApplyAndBases ''FlatRowExtends+makeDerivings [''Eq, ''Ord] [''RowExtend]+makeInstances [''Binary, ''NFData] [''RowExtend]++instance+    Constraints (RowExtend key val rest h) Show =>+    Show (RowExtend key val rest h)+    where+    showsPrec p (RowExtend h v r) = (showCon "RowExtend" @| h @| v @| r) p++{-# INLINE flattenRowExtend #-}+flattenRowExtend ::+    (Ord key, Monad m) =>+    (v # rest -> m (Maybe (RowExtend key val rest # v))) ->+    RowExtend key val rest # v ->+    m (FlatRowExtends key val rest # v)+flattenRowExtend nextExtend (RowExtend h v rest) =+    flattenRow nextExtend rest+        <&> freExtends %~ Map.unionWith (error "Colliding keys") (Map.singleton h v)++{-# INLINE flattenRow #-}+flattenRow ::+    (Ord key, Monad m) =>+    (v # rest -> m (Maybe (RowExtend key val rest # v))) ->+    v # rest ->+    m (FlatRowExtends key val rest # v)+flattenRow nextExtend x =+    nextExtend x+        >>= maybe (pure (FlatRowExtends mempty x)) (flattenRowExtend nextExtend)++{-# INLINE unflattenRow #-}+unflattenRow ::+    Monad m =>+    (RowExtend key val rest # v -> m (v # rest)) ->+    FlatRowExtends key val rest # v ->+    m (v # rest)+unflattenRow mkExtend (FlatRowExtends fields rest) =+    fields ^@.. Lens.itraversed & foldM f rest+    where+        f acc (key, val) = RowExtend key val acc & mkExtend++-- Helpers for Unify instances of type-level RowExtends:++{-# INLINE verifyRowExtendConstraints #-}+verifyRowExtendConstraints ::+    RowConstraints (TypeConstraintsOf rowTyp) =>+    (TypeConstraintsOf rowTyp -> TypeConstraintsOf valTyp) ->+    TypeConstraintsOf rowTyp ->+    RowExtend (RowKey rowTyp) valTyp rowTyp # h ->+    Maybe (RowExtend (RowKey rowTyp) valTyp rowTyp # WithConstraint h)+verifyRowExtendConstraints toChildC c (RowExtend h v rest)+    | c ^. forbidden . contains h = Nothing+    | otherwise =+        RowExtend+            h+            (WithConstraint (c & forbidden .~ mempty & toChildC) v)+            (WithConstraint (c & forbidden . contains h .~ True) rest)+            & Just++{-# INLINE rowExtendStructureMismatch #-}+rowExtendStructureMismatch ::+    Ord key =>+    ( Unify m rowTyp+    , Unify m valTyp+    ) =>+    (forall c. Unify m c => UVarOf m # c -> UVarOf m # c -> m (UVarOf m # c)) ->+    Prism' (rowTyp # UVarOf m) (RowExtend key valTyp rowTyp # UVarOf m) ->+    RowExtend key valTyp rowTyp # UVarOf m ->+    RowExtend key valTyp rowTyp # UVarOf m ->+    m ()+rowExtendStructureMismatch match extend r0 r1 =+    do+        flat0 <- flattenRowExtend nextExtend r0+        flat1 <- flattenRowExtend nextExtend r1+        Map.intersectionWith match (flat0 ^. freExtends) (flat1 ^. freExtends)+            & sequenceA_+        restVar <- UUnbound mempty & newVar binding+        let side x y =+                unflattenRow+                    mkExtend+                    FlatRowExtends+                        { _freExtends =+                            (x ^. freExtends) `Map.difference` (y ^. freExtends)+                        , _freRest = restVar+                        }+                    >>= match (y ^. freRest)+        _ <- side flat0 flat1+        _ <- side flat1 flat0+        pure ()+    where+        mkExtend ext = UTermBody mempty (extend # ext) & UTerm & newVar binding+        nextExtend v = semiPruneLookup v <&> (^? Lens._2 . _UTerm . uBody . extend)++-- Helper for infering row usages of a row element,+-- such as getting a field from a record or injecting into a sum type.+-- Returns a unification variable for the element and for the whole row.+{-# INLINE rowElementInfer #-}+rowElementInfer ::+    forall m valTyp rowTyp.+    ( UnifyGen m valTyp+    , UnifyGen m rowTyp+    , RowConstraints (TypeConstraintsOf rowTyp)+    ) =>+    (RowExtend (RowKey rowTyp) valTyp rowTyp # UVarOf m -> rowTyp # UVarOf m) ->+    RowKey rowTyp ->+    m (UVarOf m # valTyp, UVarOf m # rowTyp)+rowElementInfer extendToRow h =+    do+        restVar <-+            scopeConstraints (Proxy @rowTyp)+                >>= newVar binding . UUnbound . (forbidden . contains h .~ True)+        part <- newUnbound+        whole <- RowExtend h part restVar & extendToRow & newTerm+        pure (part, whole)

@@ -0,0 +1,279 @@+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE UndecidableInstances #-}++-- | Type schemes+module Hyper.Syntax.Scheme+    ( Scheme (..)+    , sForAlls+    , sTyp+    , W_Scheme (..)+    , QVars (..)+    , _QVars+    , HasScheme (..)+    , loadScheme+    , saveScheme+    , MonadInstantiate (..)+    , inferType+    , QVarInstances (..)+    , _QVarInstances+    , makeQVarInstances+    ) where++import qualified Control.Lens as Lens+import Control.Monad.Trans.Class (MonadTrans (..))+import Control.Monad.Trans.State (StateT (..))+import qualified Data.Map as Map+import Hyper+import Hyper.Class.Optic (HNodeLens (..))+import Hyper.Infer+import Hyper.Recurse+import Hyper.Unify+import Hyper.Unify.Generalize+import Hyper.Unify.New (newTerm)+import Hyper.Unify.QuantifiedVar (HasQuantifiedVar (..), MonadQuantify (..), OrdQVar)+import Hyper.Unify.Term (UTerm (..), uBody)+import Text.PrettyPrint ((<+>))+import qualified Text.PrettyPrint as Pretty+import Text.PrettyPrint.HughesPJClass (Pretty (..), maybeParens)++import Hyper.Internal.Prelude++-- | A type scheme representing a polymorphic type.+data Scheme varTypes typ h = Scheme+    { _sForAlls :: varTypes # QVars+    , _sTyp :: h :# typ+    }+    deriving (Generic)++newtype QVars typ+    = QVars+        (Map (QVar (GetHyperType typ)) (TypeConstraintsOf (GetHyperType typ)))+    deriving stock (Generic)++newtype QVarInstances h typ = QVarInstances (Map (QVar (GetHyperType typ)) (h typ))+    deriving stock (Generic)++makeLenses ''Scheme+makePrisms ''QVars+makePrisms ''QVarInstances+makeCommonInstances [''Scheme, ''QVars, ''QVarInstances]+makeHTraversableApplyAndBases ''Scheme++instance RNodes t => RNodes (Scheme v t)+instance (c (Scheme v t), Recursively c t) => Recursively c (Scheme v t)+instance (HTraversable (Scheme v t), RTraversable t) => RTraversable (Scheme v t)++instance+    ( Ord (QVar (GetHyperType typ))+    , Semigroup (TypeConstraintsOf (GetHyperType typ))+    ) =>+    Semigroup (QVars typ)+    where+    QVars m <> QVars n = QVars (Map.unionWith (<>) m n)++instance+    ( Ord (QVar (GetHyperType typ))+    , Semigroup (TypeConstraintsOf (GetHyperType typ))+    ) =>+    Monoid (QVars typ)+    where+    mempty = QVars mempty++instance+    (Pretty (varTypes # QVars), Pretty (h :# typ)) =>+    Pretty (Scheme varTypes typ h)+    where+    pPrintPrec lvl p (Scheme forAlls typ)+        | Pretty.isEmpty f = pPrintPrec lvl p typ+        | otherwise = f <+> pPrintPrec lvl 0 typ & maybeParens (p > 0)+        where+            f = pPrintPrec lvl 0 forAlls++instance+    (Pretty (TypeConstraintsOf typ), Pretty (QVar typ)) =>+    Pretty (QVars # typ)+    where+    pPrint (QVars qvars) =+        qvars ^@.. Lens.itraversed+            <&> (<> Pretty.text ".") . (Pretty.text "∀" <>) . printVar+            & Pretty.hsep+        where+            printVar (q, c)+                | cP == mempty = pPrint q+                | otherwise = pPrint q <> Pretty.text "(" <> cP <> Pretty.text ")"+                where+                    cP = pPrint c++type instance Lens.Index (QVars typ) = QVar (GetHyperType typ)+type instance Lens.IxValue (QVars typ) = TypeConstraintsOf (GetHyperType typ)++instance Ord (QVar (GetHyperType typ)) => Lens.Ixed (QVars typ)++instance Ord (QVar (GetHyperType typ)) => Lens.At (QVars typ) where+    at h = _QVars . Lens.at h++type instance InferOf (Scheme _ t) = HFlip GTerm t++class UnifyGen m t => MonadInstantiate m t where+    localInstantiations ::+        QVarInstances (UVarOf m) # t ->+        m a ->+        m a+    lookupQVar :: QVar t -> m (UVarOf m # t)++instance+    ( HasInferredValue typ+    , UnifyGen m typ+    , HTraversable varTypes+    , HNodesConstraint varTypes (MonadInstantiate m)+    , Infer m typ+    ) =>+    Infer m (Scheme varTypes typ)+    where+    {-# INLINE inferBody #-}+    inferBody (Scheme vars typ) =+        do+            foralls <- htraverse (Proxy @(MonadInstantiate m) #> makeQVarInstances) vars+            let withForalls =+                    hfoldMap+                        (Proxy @(MonadInstantiate m) #> (: []) . localInstantiations)+                        foralls+                        & foldl (.) id+            InferredChild typI typR <- inferChild typ & withForalls+            generalize (typR ^. inferredValue)+                <&> (Scheme vars typI,) . MkHFlip++inferType ::+    ( InferOf t ~ ANode t+    , HNodesConstraint t HasInferredValue+    , MonadInstantiate m t+    ) =>+    t # InferChild m h ->+    m (t # h, InferOf t # UVarOf m)+inferType x =+    case x ^? quantifiedVar of+        Just q -> lookupQVar q <&> (quantifiedVar # q,) . MkANode+        Nothing ->+            do+                xI <- htraverse (const inferChild) x+                hmap (Proxy @HasInferredValue #> (^. inType . inferredValue)) xI+                    & newTerm+                    <&> (hmap (const (^. inRep)) xI,) . MkANode++{-# INLINE makeQVarInstances #-}+makeQVarInstances ::+    Unify m typ =>+    QVars # typ ->+    m (QVarInstances (UVarOf m) # typ)+makeQVarInstances (QVars foralls) =+    traverse (newVar binding . USkolem) foralls <&> QVarInstances++{-# INLINE loadBody #-}+loadBody ::+    ( UnifyGen m typ+    , HNodeLens varTypes typ+    , Ord (QVar typ)+    ) =>+    varTypes # QVarInstances (UVarOf m) ->+    typ # GTerm (UVarOf m) ->+    m (GTerm (UVarOf m) # typ)+loadBody foralls x =+    case x ^? quantifiedVar >>= getForAll of+        Just r -> GPoly r & pure+        Nothing ->+            case htraverse (const (^? _GMono)) x of+                Just xm -> newTerm xm <&> GMono+                Nothing -> GBody x & pure+    where+        getForAll v = foralls ^? hNodeLens . _QVarInstances . Lens.ix v++class+    (UnifyGen m t, HNodeLens varTypes t, Ord (QVar t)) =>+    HasScheme varTypes m t+    where+    hasSchemeRecursive :: Proxy varTypes -> Proxy m -> RecMethod (HasScheme varTypes m) t+    {-# INLINE hasSchemeRecursive #-}+    default hasSchemeRecursive ::+        HNodesConstraint t (HasScheme varTypes m) =>+        Proxy varTypes ->+        Proxy m ->+        RecMethod (HasScheme varTypes m) t+    hasSchemeRecursive _ _ _ = Dict++instance Recursive (HasScheme varTypes m) where+    recurse = hasSchemeRecursive (Proxy @varTypes) (Proxy @m) . proxyArgument++-- | Load scheme into unification monad so that different instantiations share+-- the scheme's monomorphic parts -+-- their unification is O(1) as it is the same shared unification term.+{-# INLINE loadScheme #-}+loadScheme ::+    forall m varTypes typ.+    ( HTraversable varTypes+    , HNodesConstraint varTypes (UnifyGen m)+    , HasScheme varTypes m typ+    ) =>+    Pure # Scheme varTypes typ ->+    m (GTerm (UVarOf m) # typ)+loadScheme (Pure (Scheme vars typ)) =+    do+        foralls <- htraverse (Proxy @(UnifyGen m) #> makeQVarInstances) vars+        wrapM (Proxy @(HasScheme varTypes m) #>> loadBody foralls) typ++saveH ::+    forall typ varTypes m.+    HasScheme varTypes m typ =>+    GTerm (UVarOf m) # typ ->+    StateT (varTypes # QVars, [m ()]) m (Pure # typ)+saveH (GBody x) =+    htraverse (Proxy @(HasScheme varTypes m) #> saveH) x+        <&> (_Pure #)+        \\ hasSchemeRecursive (Proxy @varTypes) (Proxy @m) (Proxy @typ)+saveH (GMono x) =+    unwrapM (Proxy @(HasScheme varTypes m) #>> f) x & lift+    where+        f v =+            semiPruneLookup v+                <&> \case+                    (_, UTerm t) -> t ^. uBody+                    (_, UUnbound{}) -> error "saveScheme of non-toplevel scheme!"+                    _ -> error "unexpected state at saveScheme of monomorphic part"+saveH (GPoly x) =+    lookupVar binding x+        & lift+        >>= \case+            USkolem l ->+                do+                    r <-+                        scopeConstraints (Proxy @typ)+                            <&> (<> l)+                            >>= newQuantifiedVariable+                            & lift+                    Lens._1+                        . hNodeLens+                        %= (\v -> v & _QVars . Lens.at r ?~ generalizeConstraints l :: QVars # typ)+                    Lens._2 %= (bindVar binding x (USkolem l) :)+                    let result = _Pure . quantifiedVar # r+                    UResolved result & bindVar binding x & lift+                    pure result+            UResolved v -> pure v+            _ -> error "unexpected state at saveScheme's forall"++saveScheme ::+    ( HNodesConstraint varTypes OrdQVar+    , HPointed varTypes+    , HasScheme varTypes m typ+    ) =>+    GTerm (UVarOf m) # typ ->+    m (Pure # Scheme varTypes typ)+saveScheme x =+    do+        (t, (v, recover)) <-+            runStateT+                (saveH x)+                ( hpure (Proxy @OrdQVar #> QVars mempty)+                , []+                )+        _Pure # Scheme v t <$ sequence_ recover

@@ -0,0 +1,119 @@+{-# LANGUAGE FlexibleContexts #-}++-- | Alpha-equality for schemes+module Hyper.Syntax.Scheme.AlphaEq+    ( alphaEq+    ) where++import Control.Lens (ix)+import Hyper+import Hyper.Class.Optic (HNodeLens (..))+import Hyper.Class.ZipMatch (zipMatch_)+import Hyper.Recurse (wrapM, (#>>))+import Hyper.Syntax.Scheme+import Hyper.Unify+import Hyper.Unify.New (newTerm)+import Hyper.Unify.QuantifiedVar+import Hyper.Unify.Term (UTerm (..), uBody)++import Hyper.Internal.Prelude++makeQVarInstancesInScope ::+    forall m typ.+    UnifyGen m typ =>+    QVars # typ ->+    m (QVarInstances (UVarOf m) # typ)+makeQVarInstancesInScope (QVars foralls) =+    traverse makeSkolem foralls <&> QVarInstances+    where+        makeSkolem c = scopeConstraints (Proxy @typ) >>= newVar binding . USkolem . (c <>)++schemeBodyToType ::+    (UnifyGen m typ, HNodeLens varTypes typ, Ord (QVar typ)) =>+    varTypes # QVarInstances (UVarOf m) ->+    typ # UVarOf m ->+    m (UVarOf m # typ)+schemeBodyToType foralls x =+    case x ^? quantifiedVar >>= getForAll of+        Nothing -> newTerm x+        Just r -> pure r+    where+        getForAll v = foralls ^? hNodeLens . _QVarInstances . ix v++schemeToRestrictedType ::+    forall m varTypes typ.+    ( HTraversable varTypes+    , HNodesConstraint varTypes (UnifyGen m)+    , HasScheme varTypes m typ+    ) =>+    Pure # Scheme varTypes typ ->+    m (UVarOf m # typ)+schemeToRestrictedType (Pure (Scheme vars typ)) =+    do+        foralls <- htraverse (Proxy @(UnifyGen m) #> makeQVarInstancesInScope) vars+        wrapM (Proxy @(HasScheme varTypes m) #>> schemeBodyToType foralls) typ++goUTerm ::+    forall m t.+    Unify m t =>+    UVarOf m # t ->+    UTerm (UVarOf m) # t ->+    UVarOf m # t ->+    UTerm (UVarOf m) # t ->+    m ()+goUTerm xv USkolem{} yv USkolem{} =+    do+        bindVar binding xv (UInstantiated yv)+        bindVar binding yv (UInstantiated xv)+goUTerm xv (UInstantiated xt) yv (UInstantiated yt)+    | xv == yt && yv == xt = pure ()+    | otherwise = unifyError (SkolemEscape xv)+goUTerm xv USkolem{} yv UUnbound{} = bindVar binding yv (UToVar xv)+goUTerm xv UUnbound{} yv USkolem{} = bindVar binding xv (UToVar yv)+goUTerm xv UInstantiated{} yv UUnbound{} = bindVar binding yv (UToVar xv)+goUTerm xv UUnbound{} yv UInstantiated{} = bindVar binding xv (UToVar yv)+goUTerm _ (UToVar xv) yv yu =+    do+        xu <- lookupVar binding xv+        goUTerm xv xu yv yu+goUTerm xv xu _ (UToVar yv) =+    do+        yu <- lookupVar binding yv+        goUTerm xv xu yv yu+goUTerm xv USkolem{} yv _ = unifyError (SkolemUnified xv yv)+goUTerm xv _ yv USkolem{} = unifyError (SkolemUnified yv xv)+goUTerm xv UInstantiated{} yv _ = unifyError (SkolemUnified xv yv)+goUTerm xv _ yv UInstantiated{} = unifyError (SkolemUnified yv xv)+goUTerm xv UUnbound{} yv yu = goUTerm xv yu yv yu -- Term created in structure mismatch+goUTerm xv xu yv UUnbound{} = goUTerm xv xu yv xu -- Term created in structure mismatch+goUTerm _ (UTerm xt) _ (UTerm yt) =+    zipMatch_ (Proxy @(Unify m) #> goUVar) (xt ^. uBody) (yt ^. uBody)+        & fromMaybe (structureMismatch (\x y -> x <$ goUVar x y) (xt ^. uBody) (yt ^. uBody))+        \\ unifyRecursive (Proxy @m) (Proxy @t)+goUTerm _ _ _ _ = error "unexpected state at alpha-eq"++goUVar ::+    Unify m t =>+    UVarOf m # t ->+    UVarOf m # t ->+    m ()+goUVar xv yv =+    do+        xu <- lookupVar binding xv+        yu <- lookupVar binding yv+        goUTerm xv xu yv yu++-- Check for alpha equality. Raises a `unifyError` when mismatches.+alphaEq ::+    ( HTraversable varTypes+    , HNodesConstraint varTypes (UnifyGen m)+    , HasScheme varTypes m typ+    ) =>+    Pure # Scheme varTypes typ ->+    Pure # Scheme varTypes typ ->+    m ()+alphaEq s0 s1 =+    do+        t0 <- schemeToRestrictedType s0+        t1 <- schemeToRestrictedType s1+        goUVar t0 t1

@@ -0,0 +1,69 @@+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE UndecidableInstances #-}++-- | Type signatures+module Hyper.Syntax.TypeSig+    ( TypeSig (..)+    , tsType+    , tsTerm+    , W_TypeSig (..)+    ) where++import Generics.Constraints (Constraints)+import Hyper+import Hyper.Infer+import Hyper.Syntax.Scheme+import Hyper.Unify (UnifyGen, unify)+import Hyper.Unify.Generalize (instantiateWith)+import Hyper.Unify.Term (UTerm (..))+import Text.PrettyPrint ((<+>))+import qualified Text.PrettyPrint as Pretty+import Text.PrettyPrint.HughesPJClass (Pretty (..), maybeParens)++import Hyper.Internal.Prelude++data TypeSig vars term h = TypeSig+    { _tsTerm :: h :# term+    , _tsType :: h :# Scheme vars (TypeOf term)+    }+    deriving (Generic)++makeLenses ''TypeSig+makeCommonInstances [''TypeSig]+makeHTraversableApplyAndBases ''TypeSig++instance+    Constraints (TypeSig vars term h) Pretty =>+    Pretty (TypeSig vars term h)+    where+    pPrintPrec lvl p (TypeSig term typ) =+        pPrintPrec lvl 1 term <+> Pretty.text ":" <+> pPrintPrec lvl 1 typ+            & maybeParens (p > 1)++type instance InferOf (TypeSig _ t) = InferOf t++instance+    ( MonadScopeLevel m+    , HasInferredType term+    , HasInferredValue (TypeOf term)+    , HTraversable vars+    , HTraversable (InferOf term)+    , HNodesConstraint (InferOf term) (UnifyGen m)+    , HNodesConstraint vars (MonadInstantiate m)+    , UnifyGen m (TypeOf term)+    , Infer m (TypeOf term)+    , Infer m term+    ) =>+    Infer m (TypeSig vars term)+    where+    inferBody (TypeSig x s) =+        do+            InferredChild xI xR <- inferChild x+            InferredChild sI sR <- inferChild s+            (t, ()) <- instantiateWith (pure ()) USkolem (sR ^. _HFlip)+            xR+                & inferredType (Proxy @term) #%%~ unify t+                <&> (TypeSig xI sI,)+            & localLevel

@@ -0,0 +1,82 @@+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE UndecidableInstances #-}++module Hyper.Syntax.TypedLam+    ( TypedLam (..)+    , tlIn+    , tlInType+    , tlOut+    , W_TypedLam (..)+    , MorphWitness (..)+    ) where++import Generics.Constraints (Constraints)+import Hyper+import Hyper.Class.Optic (HNodeLens (..), HSubset (..), HSubset')+import Hyper.Infer+import Hyper.Syntax.FuncType (FuncType (..))+import Hyper.Unify (UVarOf, UnifyGen)+import Hyper.Unify.New (newTerm)+import qualified Text.PrettyPrint as P+import Text.PrettyPrint.HughesPJClass (Pretty (..), maybeParens)++import Hyper.Internal.Prelude++data TypedLam var typ expr h = TypedLam+    { _tlIn :: var+    , _tlInType :: h :# typ+    , _tlOut :: h :# expr+    }+    deriving (Generic)++makeLenses ''TypedLam+makeCommonInstances [''TypedLam]+makeHTraversableApplyAndBases ''TypedLam+makeZipMatch ''TypedLam+makeHContext ''TypedLam+makeHMorph ''TypedLam++instance (RNodes t, RNodes e) => RNodes (TypedLam v t e)+instance+    (c (TypedLam v t e), Recursively c t, Recursively c e) =>+    Recursively c (TypedLam v t e)+instance (RTraversable t, RTraversable e) => RTraversable (TypedLam v t e)++instance+    Constraints (TypedLam var typ expr h) Pretty =>+    Pretty (TypedLam var typ expr h)+    where+    pPrintPrec lvl p (TypedLam i t o) =+        ( P.text "λ"+            <> pPrintPrec lvl 0 i+            <> P.text ":"+            <> pPrintPrec lvl 0 t+        )+            P.<+> P.text "→"+            P.<+> pPrintPrec lvl 0 o+            & maybeParens (p > 0)++type instance InferOf (TypedLam _ _ e) = ANode (TypeOf e)++instance+    ( Infer m t+    , Infer m e+    , HasInferredType e+    , UnifyGen m (TypeOf e)+    , HSubset' (TypeOf e) (FuncType (TypeOf e))+    , HNodeLens (InferOf t) (TypeOf e)+    , LocalScopeType v (UVarOf m # TypeOf e) m+    ) =>+    Infer m (TypedLam v t e)+    where+    {-# INLINE inferBody #-}+    inferBody (TypedLam p t r) =+        do+            InferredChild tI tR <- inferChild t+            let tT = tR ^. hNodeLens+            InferredChild rI rR <- inferChild r & localScopeType p tT+            hSubset # FuncType tT (rR ^# inferredType (Proxy @e))+                & newTerm+                <&> (TypedLam p tI rI,) . MkANode

@@ -0,0 +1,70 @@+{-# LANGUAGE EmptyCase #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE UndecidableInstances #-}++-- | Variables.+module Hyper.Syntax.Var+    ( Var (..)+    , _Var+    , VarType (..)+    , ScopeOf+    , HasScope (..)+    ) where++import Hyper+import Hyper.Infer+import Hyper.Unify (UVarOf, UnifyGen)+import Text.PrettyPrint.HughesPJClass (Pretty (..))++import Hyper.Internal.Prelude++type family ScopeOf (t :: HyperType) :: HyperType++class HasScope m s where+    getScope :: m (s # UVarOf m)++class VarType var expr where+    -- | Instantiate a type for a variable in a given scope+    varType ::+        UnifyGen m (TypeOf expr) =>+        Proxy expr ->+        var ->+        ScopeOf expr # UVarOf m ->+        m (UVarOf m # TypeOf expr)++-- | Parameterized by term AST and not by its type AST+-- (which currently is its only part used),+-- for future evaluation/complilation support.+newtype Var v (expr :: HyperType) (h :: AHyperType) = Var v+    deriving newtype (Eq, Ord, Binary, NFData)+    deriving stock (Show, Generic)++makePrisms ''Var+makeHTraversableApplyAndBases ''Var+makeZipMatch ''Var+makeHContext ''Var+makeHMorph ''Var++instance Pretty v => Pretty (Var v expr h) where+    pPrintPrec lvl p (Var v) = pPrintPrec lvl p v++type instance InferOf (Var _ t) = ANode (TypeOf t)++instance HasInferredType (Var v t) where+    type TypeOf (Var v t) = TypeOf t+    {-# INLINE inferredType #-}+    inferredType _ = _ANode++instance+    ( UnifyGen m (TypeOf expr)+    , HasScope m (ScopeOf expr)+    , VarType v expr+    , Monad m+    ) =>+    Infer m (Var v expr)+    where+    {-# INLINE inferBody #-}+    inferBody (Var x) =+        getScope >>= varType (Proxy @expr) x <&> (Var x,) . MkANode

@@ -1,23 +1,22 @@ {-# LANGUAGE TemplateHaskell #-}  -- | Generate 'HApply' and related instances via @TemplateHaskell@- module Hyper.TH.Apply     ( makeHApply     , makeHApplyAndBases     , makeHApplicativeBases     ) where -import           Control.Applicative (liftA2)+import Control.Applicative (liftA2) import qualified Control.Lens as Lens-import           Hyper.Class.Apply (HApply(..))-import           Hyper.TH.Functor (makeHFunctor)-import           Hyper.TH.Internal.Utils-import           Hyper.TH.Nodes (makeHNodes)-import           Hyper.TH.Pointed (makeHPointed)-import           Language.Haskell.TH+import Hyper.Class.Apply (HApply (..))+import Hyper.TH.Functor (makeHFunctor)+import Hyper.TH.Internal.Utils+import Hyper.TH.Nodes (makeHNodes)+import Hyper.TH.Pointed (makeHPointed)+import Language.Haskell.TH -import           Hyper.Internal.Prelude+import Hyper.Internal.Prelude  -- | Generate instances of 'HApply', -- 'Hyper.Class.Functor.HFunctor', 'Hyper.Class.Pointed.HPointed' and 'Hyper.Class.Nodes.HNodes',@@ -25,19 +24,21 @@ makeHApplicativeBases :: Name -> DecsQ makeHApplicativeBases x =     sequenceA-    [ makeHPointed x-    , makeHApplyAndBases x-    ] <&> concat+        [ makeHPointed x+        , makeHApplyAndBases x+        ]+        <&> concat  -- | Generate an instance of 'HApply' -- along with its bases 'Hyper.Class.Functor.HFunctor' and 'Hyper.Class.Nodes.HNodes' makeHApplyAndBases :: Name -> DecsQ makeHApplyAndBases x =     sequenceA-    [ makeHNodes x-    , makeHFunctor x-    , makeHApply x-    ] <&> concat+        [ makeHNodes x+        , makeHFunctor x+        , makeHApply x+        ]+        <&> concat  -- | Generate an instance of 'HApply' makeHApply :: Name -> DecsQ@@ -48,20 +49,25 @@     do         (name, _, fields) <-             case tiConstructors info of-            [x] -> pure x-            _ -> fail "makeHApply only supports types with a single constructor"+                [x] -> pure x+                _ -> fail "makeHApply only supports types with a single constructor"         let xVars = makeConstructorVars "x" fields         let yVars = makeConstructorVars "y" fields-        instanceD (makeContext info >>= simplifyContext) [t|HApply $(pure (tiInstance info))|]+        instanceD+            (makeContext info >>= simplifyContext)+            [t|HApply $(pure (tiInstance info))|]             [ InlineP 'hzip Inline FunLike AllPhases & PragmaD & pure-            , funD 'hzip+            , funD+                'hzip                 [ clause                     [ consPat name xVars                     , consPat name yVars-                    ] (normalB (foldl appE (conE name) (zipWith f xVars yVars))) []+                    ]+                    (normalB (foldl appE (conE name) (zipWith f xVars yVars)))+                    []                 ]             ]-            <&> (:[])+            <&> (: [])     where         bodyFor (Right x) = bodyForPat x         bodyFor Left{} = [|(<>)|]@@ -76,8 +82,8 @@     tiConstructors info >>= (^. Lens._3) & traverse ctxFor <&> mconcat     where         ctxFor (Right x) = ctxForPat x-        ctxFor (Left x) = [t|Semigroup $(pure x)|] <&> (:[])+        ctxFor (Left x) = [t|Semigroup $(pure x)|] <&> (: [])         ctxForPat (InContainer t pat) = (:) <$> [t|Applicative $(pure t)|] <*> ctxForPat pat-        ctxForPat (GenEmbed t) = [t|HApply $(pure t)|] <&> (:[])+        ctxForPat (GenEmbed t) = [t|HApply $(pure t)|] <&> (: [])         ctxForPat (FlatEmbed t) = makeContext t         ctxForPat _ = pure []

@@ -5,25 +5,27 @@     ) where  import qualified Control.Lens as Lens-import           Hyper.Class.Context (HContext(..))-import           Hyper.Class.Functor (HFunctor(..))-import           Hyper.Combinator.Func (HFunc(..), _HFunc)-import           Hyper.TH.Internal.Utils-import           Language.Haskell.TH-import           Language.Haskell.TH.Datatype (ConstructorVariant(..))+import Hyper.Class.Context (HContext (..))+import Hyper.Class.Functor (HFunctor (..))+import Hyper.Combinator.Func (HFunc (..), _HFunc)+import Hyper.TH.Internal.Utils+import Language.Haskell.TH+import Language.Haskell.TH.Datatype (ConstructorVariant (..)) -import           Hyper.Internal.Prelude+import Hyper.Internal.Prelude  makeHContext :: Name -> DecsQ makeHContext typeName = makeTypeInfo typeName >>= makeHContextForType  makeHContextForType :: TypeInfo -> DecsQ makeHContextForType info =-    instanceD (simplifyContext (makeContext info)) [t|HContext $(pure (tiInstance info))|]-    [ InlineP 'hcontext Inline FunLike AllPhases & PragmaD & pure-    , funD 'hcontext (tiConstructors info <&> makeHContextCtr)-    ]-    <&> (:[])+    instanceD+        (simplifyContext (makeContext info))+        [t|HContext $(pure (tiInstance info))|]+        [ InlineP 'hcontext Inline FunLike AllPhases & PragmaD & pure+        , funD 'hcontext (tiConstructors info <&> makeHContextCtr)+        ]+        <&> (: [])  makeContext :: TypeInfo -> [Pred] makeContext info =@@ -39,18 +41,25 @@ makeHContextCtr (cName, _, []) =     clause [conP cName []] (normalB (conE cName)) [] makeHContextCtr (cName, RecordConstructor fieldNames, cFields) =-    clause [varWhole `asP` conP cName (cVars <&> varP)]-    (normalB (foldl appE (conE cName) (zipWith bodyFor cFields (zip fieldNames cVars)))) []+    clause+        [varWhole `asP` conP cName (cVars <&> varP)]+        (normalB (foldl appE (conE cName) (zipWith bodyFor cFields (zip fieldNames cVars))))+        []     where         cVars =-            [(0 :: Int) ..] <&> show <&> ("_x" <>) <&> mkName-            & take (length cFields)+            [(0 :: Int) ..]+                <&> mkName . ("_x" <>) . show+                & take (length cFields)         bodyFor Left{} (_, v) = varE v         bodyFor (Right Node{}) (f, v) =-            [|HFunc-                $(lamE [varP varField]-                    [|Lens.Const $(recUpdE (varE varWhole) [pure (f, VarE varField)])|])-                :*: $(varE v)|]+            [|+                HFunc+                    $( lamE+                        [varP varField]+                        [|Lens.Const $(recUpdE (varE varWhole) [pure (f, VarE varField)])|]+                     )+                    :*: $(varE v)+                |]         bodyFor _ _ = fail "makeHContext only works for simple record fields"         varWhole = mkName "_whole"         varField = mkName "_field"@@ -65,9 +74,10 @@         bodyFor (Right FlatEmbed{}) = embed         bodyFor _ = fail "makeHContext only works for simple fields"         embed =-            [|hmap-                (const (Lens._1 . _HFunc . Lens.mapped . Lens._Wrapped Lens.%~ $n))-                (hcontext $v)-            |]+            [|+                hmap+                    (const (Lens._1 . _HFunc . Lens.mapped . Lens._Wrapped Lens.%~ $n))+                    (hcontext $v)+                |]         cVar = mkName "_c" makeHContextCtr _ = fail "makeHContext: unsupported constructor"

@@ -1,18 +1,17 @@ {-# LANGUAGE TemplateHaskell #-}  -- | Generate 'HFoldable' instances via @TemplateHaskell@- module Hyper.TH.Foldable     ( makeHFoldable     ) where  import qualified Control.Lens as Lens-import           Hyper.Class.Foldable (HFoldable(..))-import           Hyper.TH.Internal.Utils-import           Language.Haskell.TH-import           Language.Haskell.TH.Datatype (ConstructorVariant)+import Hyper.Class.Foldable (HFoldable (..))+import Hyper.TH.Internal.Utils+import Language.Haskell.TH+import Language.Haskell.TH.Datatype (ConstructorVariant) -import           Hyper.Internal.Prelude+import Hyper.Internal.Prelude  -- | Generate a 'HFoldable' instance makeHFoldable :: Name -> DecsQ@@ -20,11 +19,13 @@  makeHFoldableForType :: TypeInfo -> DecsQ makeHFoldableForType info =-    instanceD (makeContext info >>= simplifyContext) [t|HFoldable $(pure (tiInstance info))|]-    [ InlineP 'hfoldMap Inline FunLike AllPhases & PragmaD & pure-    , funD 'hfoldMap (tiConstructors info <&> makeCtr)-    ]-    <&> (:[])+    instanceD+        (makeContext info >>= simplifyContext)+        [t|HFoldable $(pure (tiInstance info))|]+        [ InlineP 'hfoldMap Inline FunLike AllPhases & PragmaD & pure+        , funD 'hfoldMap (tiConstructors info <&> makeCtr)+        ]+        <&> (: [])     where         (_, wit) = makeNodeOf info         makeCtr ctr =@@ -35,10 +36,11 @@ makeContext :: TypeInfo -> Q [Pred] makeContext info =     tiConstructors info ^.. traverse . Lens._3 . traverse . Lens._Right-    & traverse ctxForPat <&> mconcat+        & traverse ctxForPat+        <&> mconcat     where         ctxForPat (InContainer t pat) = (:) <$> [t|Foldable $(pure t)|] <*> ctxForPat pat-        ctxForPat (GenEmbed t) = [t|HFoldable $(pure t)|] <&> (:[])+        ctxForPat (GenEmbed t) = [t|HFoldable $(pure t)|] <&> (: [])         ctxForPat (FlatEmbed t) = makeContext t         ctxForPat _ = pure [] @@ -50,18 +52,20 @@     (conP cName (cVars <&> varP), body)     where         cVars =-            [i ..] <&> show <&> ("_x" <>) <&> mkName-            & take (length cFields)+            [i ..]+                <&> mkName . ("_x" <>) . show+                & take (length cFields)         bodyParts =-            zipWith (\x y -> x <&> (`appE` y))-            (cFields <&> bodyFor)-            (cVars <&> varE)-            & concat+            zipWith+                (\x y -> x <&> (`appE` y))+                (cFields <&> bodyFor)+                (cVars <&> varE)+                & concat         body =             case bodyParts of-            [] -> [|mempty|]-            _ -> foldl1 append bodyParts-            & normalB+                [] -> [|mempty|]+                _ -> foldl1 append bodyParts+                & normalB         append x y = [|$x <> $y|]         f = varE varF         bodyFor (Right x) = bodyForPat x@@ -71,8 +75,9 @@         bodyForPat (InContainer _ pat) = bodyForPat pat <&> appE [|foldMap|]         bodyForPat (FlatEmbed x) =             [ lamCaseE-                (tiConstructors x-                    <&> makeHFoldMapCtr (i + length cVars) wit-                    <&> \(p, b) -> match p b []+                ( tiConstructors x+                    <&> uncurry match+                        . makeHFoldMapCtr (i + length cVars) wit+                        ?? []                 )             ]

@@ -1,18 +1,17 @@ {-# LANGUAGE TemplateHaskell #-}  -- | Generate 'HFunctor' instances via @TemplateHaskell@- module Hyper.TH.Functor     ( makeHFunctor     ) where  import qualified Control.Lens as Lens-import           Hyper.Class.Functor (HFunctor(..))-import           Hyper.TH.Internal.Utils-import           Language.Haskell.TH-import           Language.Haskell.TH.Datatype (ConstructorVariant)+import Hyper.Class.Functor (HFunctor (..))+import Hyper.TH.Internal.Utils+import Language.Haskell.TH+import Language.Haskell.TH.Datatype (ConstructorVariant) -import           Hyper.Internal.Prelude+import Hyper.Internal.Prelude  -- | Generate a 'HFunctor' instance makeHFunctor :: Name -> DecsQ@@ -20,11 +19,13 @@  makeHFunctorForType :: TypeInfo -> DecsQ makeHFunctorForType info =-    instanceD (makeContext info >>= simplifyContext) [t|HFunctor $(pure (tiInstance info))|]-    [ InlineP 'hmap Inline FunLike AllPhases & PragmaD & pure-    , funD 'hmap (tiConstructors info <&> makeCtr)-    ]-    <&> (:[])+    instanceD+        (makeContext info >>= simplifyContext)+        [t|HFunctor $(pure (tiInstance info))|]+        [ InlineP 'hmap Inline FunLike AllPhases & PragmaD & pure+        , funD 'hmap (tiConstructors info <&> makeCtr)+        ]+        <&> (: [])     where         (_, wit) = makeNodeOf info         makeCtr ctr =@@ -38,10 +39,11 @@ makeContext :: TypeInfo -> Q [Pred] makeContext info =     tiConstructors info ^.. traverse . Lens._3 . traverse . Lens._Right-    & traverse ctxForPat <&> mconcat+        & traverse ctxForPat+        <&> mconcat     where         ctxForPat (InContainer t pat) = (:) <$> [t|Functor $(pure t)|] <*> ctxForPat pat-        ctxForPat (GenEmbed t) = [t|HFunctor $(pure t)|] <&> (:[])+        ctxForPat (GenEmbed t) = [t|HFunctor $(pure t)|] <&> (: [])         ctxForPat (FlatEmbed t) = makeContext t         ctxForPat _ = pure [] @@ -50,12 +52,13 @@     (conP cName (cVars <&> varP), body)     where         cVars =-            [i ..] <&> show <&> ('x':) <&> mkName-            & take (length cFields)+            [i ..]+                <&> mkName . ('x' :) . show+                & take (length cFields)         body =             zipWith bodyFor cFields cVars-            & foldl appE (conE cName)-            & normalB+                & foldl appE (conE cName)+                & normalB         bodyFor (Right x) v = bodyForPat x `appE` varE v         bodyFor Left{} v = varE v         f = varE varF@@ -64,7 +67,8 @@         bodyForPat (InContainer _ pat) = [|fmap $(bodyForPat pat)|]         bodyForPat (FlatEmbed x) =             lamCaseE-            (tiConstructors x-                <&> makeHMapCtr (i + length cVars) wit-                <&> \(p, b) -> match p b []-            )+                ( tiConstructors x+                    <&> uncurry match+                        . makeHMapCtr (i + length cVars) wit+                        ?? []+                )

@@ -1,21 +1,20 @@ {-# LANGUAGE TemplateHaskell #-}  -- | Generate 'HasHPlain' instances via @TemplateHaskell@- module Hyper.TH.HasPlain     ( makeHasHPlain     ) where  import qualified Control.Lens as Lens import qualified Data.Map as Map-import           Hyper.Class.HasPlain-import           Hyper.TH.Internal.Utils-import           Hyper.Type (GetHyperType)-import           Hyper.Type.Pure (Pure(..), _Pure)-import           Language.Haskell.TH+import Hyper.Class.HasPlain+import Hyper.TH.Internal.Utils+import Hyper.Type (GetHyperType)+import Hyper.Type.Pure (Pure (..), _Pure)+import Language.Haskell.TH import qualified Language.Haskell.TH.Datatype as D -import           Hyper.Internal.Prelude+import Hyper.Internal.Prelude  -- | Generate a 'HasHPlain' instance makeHasHPlain :: [Name] -> DecsQ@@ -31,22 +30,24 @@         let typs = ctrs >>= (^. Lens._4) & filter (not . anHPlainOfCons)         let plains =                 typs-                >>=-                \case-                ConT hplain `AppT` x | hplain == ''HPlain -> [x]-                _ -> []+                    >>= \case+                        ConT hplain `AppT` x | hplain == ''HPlain -> [x]+                        _ -> []         plainsCtx <- plains <&> AppT (ConT ''HasHPlain) & simplifyContext         showCtx <- typs <&> AppT (ConT ''Show) & simplifyContext         let makeDeriv cls =                 standaloneDerivD-                (typs <&> AppT (ConT cls) & simplifyContext)-                [t|$(conT cls) (HPlain $(pure (tiInstance info)))|]-        (:) <$> instanceD+                    (typs <&> AppT (ConT cls) & simplifyContext)+                    [t|$(conT cls) (HPlain $(pure (tiInstance info)))|]+        (:)+            <$> instanceD                 (pure (showCtx <> plainsCtx))-                [t|HasHPlain $(pure (tiInstance  info))|]+                [t|HasHPlain $(pure (tiInstance info))|]                 [ dataInstD (pure []) ''HPlain [pure (tiInstance info)] Nothing (ctrs <&> pure . (^. Lens._1)) []-                , funD 'hPlain-                    [ clause []+                , funD+                    'hPlain+                    [ clause+                        []                         (normalB [|Lens.iso $(varE fromPlain) $(varE toPlain) . Lens.from _Pure|])                         [ funD toPlain (ctrs <&> (^. Lens._2))                         , funD fromPlain (ctrs <&> (^. Lens._3))@@ -58,8 +59,8 @@         anHPlainOfCons (ConT hplain `AppT` x)             | hplain == ''HPlain =                 case unapply x of-                (ConT{}, _) -> True-                _ -> False+                    (ConT{}, _) -> True+                    _ -> False         anHPlainOfCons _ = False         toPlain = mkName "toPlain"         fromPlain = mkName "fromPlain"@@ -87,66 +88,72 @@     Q (Con, ClauseQ, ClauseQ, [Type]) makeCtr top param (cName, _, cFields) =     traverse (forField True) cFields-    <&>-    \xs ->-    let plainTypes = xs >>= plainFieldTypes-        cVars = [0::Int ..] <&> show <&> ('x':) <&> mkName & take (length plainTypes)-    in-    ( plainTypes-        <&> (Bang NoSourceUnpackedness NoSourceStrictness, )-        & NormalC pcon-    , zipWith (>>=) (cVars <&> varE) (xs >>= toPlainFields)-        & foldl appE (conE pcon)-        & normalB-        <&> (\x -> Clause [ConP cName (toPlainPat cVars xs ^. Lens._1)] x [])-    , fromPlainFields cVars xs ^. Lens._1-        & foldl appE (conE cName)-        & normalB-        <&> \x -> Clause [ConP pcon (cVars <&> VarP)] x []-    , xs >>= fieldContext-    )+        <&> \xs ->+            let plainTypes = xs >>= plainFieldTypes+                cVars = [0 :: Int ..] <&> mkName . ('x' :) . show & take (length plainTypes)+            in  ( plainTypes+                    <&> (Bang NoSourceUnpackedness NoSourceStrictness,)+                    & NormalC pcon+                , zipWith (>>=) (cVars <&> varE) (xs >>= toPlainFields)+                    & foldl appE (conE pcon)+                    & normalB+                    & (clause [conP cName (toPlainPat cVars xs ^. Lens._1)] ?? [])+                , fromPlainFields cVars xs ^. Lens._1+                    & foldl appE (conE cName)+                    & normalB+                    & (clause [conP pcon (cVars <&> varP)] ?? [])+                , xs >>= fieldContext+                )     where         plainFieldTypes (NodeField x) = [fieldPlainType x]         plainFieldTypes (FlatFields x) = flatFields x >>= plainFieldTypes         toPlainFields (NodeField x) = [fieldToPlain x . pure]         toPlainFields (FlatFields x) = flatFields x >>= toPlainFields         toPlainPat cs [] = ([], cs)-        toPlainPat (c:cs) (NodeField{} : xs) = toPlainPat cs xs & Lens._1 %~ (VarP c :)+        toPlainPat (c : cs) (NodeField{} : xs) = toPlainPat cs xs & Lens._1 %~ (varP c :)         toPlainPat cs0 (FlatFields x : xs) =             toPlainPat cs1 xs & Lens._1 %~ (res :)             where-                res | flatIsEmbed x = embed-                    | otherwise = ConP 'Pure [embed]-                embed = ConP (flatCtr x) r+                res+                    | flatIsEmbed x = embed+                    | otherwise = conP 'Pure [embed]+                embed = conP (flatCtr x) r                 (r, cs1) = toPlainPat cs0 (flatFields x)         toPlainPat [] _ = error "out of variables"         fromPlainFields cs [] = ([], cs)-        fromPlainFields (c:cs) (NodeField x : xs) =+        fromPlainFields (c : cs) (NodeField x : xs) =             fromPlainFields cs xs & Lens._1 %~ (fieldFromPlain x (varE c) :)         fromPlainFields cs0 (FlatFields x : xs) =             fromPlainFields cs1 xs & Lens._1 %~ (res :)             where-                res | flatIsEmbed x = embed+                res+                    | flatIsEmbed x = embed                     | otherwise = [|Pure $embed|]                 embed = foldl appE (conE (flatCtr x)) r                 (r, cs1) = fromPlainFields cs0 (flatFields x)         fromPlainFields [] _ = error "out of variables"         pcon =-            show cName & reverse & takeWhile (/= '.') & reverse-            & (<> "P") & mkName+            show cName+                & reverse+                & takeWhile (/= '.')+                & reverse+                & (<> "P")+                & mkName         forField _ (Left t) =             FieldInfo-            <$> normalizeType t-            ?? id ?? id <&> NodeField+                <$> normalizeType t+                ?? id+                ?? id+                <&> NodeField         forField isTop (Right x) = forPat isTop x         forPat isTop (Node x) = forGen isTop x         forPat isTop (GenEmbed x) = forGen isTop x         forPat _ (InContainer t p) =             FieldInfo-            <$> [t|$(pure t) $(patType p)|]-            ?? (\x -> [|(hPlain #) <$> $x|])-            ?? (\x -> [|(^. hPlain) <$> $x|])-            <&> NodeField+                <$> [t|$(pure t) $(patType p)|]+                ?? (\x -> [|(hPlain #) <$> $x|])+                ?? (\x -> [|(^. hPlain) <$> $x|])+                <&> NodeField             where                 patType (Node x) = [t|HPlain $(pure x)|]                 patType (GenEmbed x) = [t|HPlain $(pure x)|]@@ -154,39 +161,35 @@                 patType (InContainer t' p') = pure t' `appT` patType p'         forPat isTop (FlatEmbed x) =             case tiConstructors x of-            [(n, _, xs)] -> traverse (forField False) xs <&> FlatInfo isTop n <&> FlatFields-            _ -> forGen isTop (tiInstance x)+                [(n, _, xs)] -> traverse (forField False) xs <&> FlatFields . FlatInfo isTop n+                _ -> forGen isTop (tiInstance x)         forGen isTop t =             case unapply t of-            (ConT c, args) ->-                reify c-                >>=-                \case-                FamilyI{} -> gen -- Not expanding type families currently-                _ ->-                    do-                        inner <- D.reifyDatatype c-                        let subst =-                                args <> [VarT param]-                                & zip (D.datatypeVars inner <&> D.tvName)-                                & Map.fromList-                        case D.datatypeCons inner of-                            [x] ->-                                D.constructorFields x-                                <&> D.applySubstitution subst-                                & traverse (matchType top param)-                                >>= traverse (forField False)-                                <&> FlatInfo isTop (D.constructorName x)-                                <&> FlatFields-                            _ -> gen-            _ -> gen+                (ConT c, args) ->+                    reify c+                        >>= \case+                            FamilyI{} -> gen -- Not expanding type families currently+                            _ ->+                                do+                                    inner <- D.reifyDatatype c+                                    let subst =+                                            args <> [VarT param]+                                                & zip (D.datatypeVars inner <&> D.tvName)+                                                & Map.fromList+                                    case D.datatypeCons inner of+                                        [x] ->+                                            traverse (matchType top param . D.applySubstitution subst) (D.constructorFields x)+                                                >>= traverse (forField False)+                                                <&> FlatFields . FlatInfo isTop (D.constructorName x)+                                        _ -> gen+                _ -> gen             where                 gen =                     FieldInfo-                    <$> [t|HPlain $(pure t)|]-                    ?? (\x -> [|hPlain # $x|])-                    ?? (\f -> [|$f ^. hPlain|])-                    <&> NodeField+                        <$> [t|HPlain $(pure t)|]+                        ?? (\x -> [|hPlain # $x|])+                        ?? (\f -> [|$f ^. hPlain|])+                        <&> NodeField         normalizeType (ConT g `AppT` VarT v)             | g == ''GetHyperType && v == param = [t|Pure|]         normalizeType (x `AppT` y) = normalizeType x `appT` normalizeType y

@@ -1,30 +1,44 @@-{-# LANGUAGE TemplateHaskell, DerivingVia #-}+{-# LANGUAGE DerivingVia #-}+{-# LANGUAGE TemplateHaskell #-}  -- Helpers for TemplateHaskell instance generators  module Hyper.TH.Internal.Utils     ( -- Internals for use in TH for sub-classes-      TypeInfo(..), TypeContents(..), CtrTypePattern(..), NodeWitnesses(..)-    , makeTypeInfo, makeNodeOf-    , parts, toTuple, matchType, niceName, mkNiceTypeName-    , applicativeStyle, unapply, getVar, makeConstructorVars-    , consPat, simplifyContext, childrenTypes+      TypeInfo (..)+    , TypeContents (..)+    , CtrTypePattern (..)+    , NodeWitnesses (..)+    , makeTypeInfo+    , makeNodeOf+    , parts+    , toTuple+    , matchType+    , niceName+    , mkNiceTypeName+    , applicativeStyle+    , unapply+    , getVar+    , makeConstructorVars+    , consPat+    , simplifyContext+    , childrenTypes     ) where  import qualified Control.Lens as Lens-import           Control.Monad.Trans.Class (MonadTrans(..))-import           Control.Monad.Trans.State (State, evalState, execStateT, gets, modify)+import Control.Monad.Trans.Class (MonadTrans (..))+import Control.Monad.Trans.State (State, evalState, execStateT, gets, modify) import qualified Data.Char as Char-import           Data.List (nub, intercalate)+import Data.List (intercalate, nub) import qualified Data.Map as Map-import           Generic.Data (Generically(..))-import           Hyper.Class.Nodes (HWitness(..))-import           Hyper.Type (AHyperType(..), GetHyperType, type (:#))-import           Language.Haskell.TH+import Generic.Data (Generically (..))+import Hyper.Class.Nodes (HWitness (..))+import Hyper.Type (AHyperType (..), GetHyperType, type (:#))+import Language.Haskell.TH import qualified Language.Haskell.TH.Datatype as D-import           Language.Haskell.TH.Datatype.TyVarBndr+import Language.Haskell.TH.Datatype.TyVarBndr -import           Hyper.Internal.Prelude+import Hyper.Internal.Prelude  data TypeInfo = TypeInfo     { tiName :: Name@@ -32,13 +46,15 @@     , tiParams :: [TyVarBndrUnit]     , tiHyperParam :: Name     , tiConstructors :: [(Name, D.ConstructorVariant, [Either Type CtrTypePattern])]-    } deriving Show+    }+    deriving (Show)  data TypeContents = TypeContents     { tcChildren :: Set Type     , tcEmbeds :: Set Type     , tcOthers :: Set Type-    } deriving (Show, Generic)+    }+    deriving (Show, Generic)     deriving (Semigroup, Monoid) via Generically TypeContents  data CtrTypePattern@@ -46,7 +62,7 @@     | FlatEmbed TypeInfo     | GenEmbed Type     | InContainer Type CtrTypePattern-    deriving Show+    deriving (Show)  makeTypeInfo :: Name -> Q TypeInfo makeTypeInfo name =@@ -55,31 +71,33 @@         (dst, var) <- parts info         let makeCons c =                 traverse (matchType name var) (D.constructorFields c)-                <&> (D.constructorName c, D.constructorVariant c, )+                    <&> (D.constructorName c,D.constructorVariant c,)         cons <- traverse makeCons (D.datatypeCons info)-        pure TypeInfo-            { tiName = name-            , tiInstance = dst-            , tiParams = D.datatypeVars info & init-            , tiHyperParam = var-            , tiConstructors = cons-            }+        pure+            TypeInfo+                { tiName = name+                , tiInstance = dst+                , tiParams = D.datatypeVars info & init+                , tiHyperParam = var+                , tiConstructors = cons+                }  parts :: D.DatatypeInfo -> Q (Type, Name) parts info =     case D.datatypeVars info of-    [] -> fail "expected type constructor which requires arguments"-    xs ->-        elimTV-        (pure . (,) res)-        ( \var c ->-            case c of-            ConT aHyper | aHyper == ''AHyperType -> pure (res, var)-            _ -> fail "expected last argument to be a AHyperType variable"-        ) (last xs)-        where-            res =-                foldl AppT (ConT (D.datatypeName info)) (init xs <&> VarT . D.tvName)+        [] -> fail "expected type constructor which requires arguments"+        xs ->+            elimTV+                (pure . (,) res)+                ( \var c ->+                    case c of+                        ConT aHyper | aHyper == ''AHyperType -> pure (res, var)+                        _ -> fail "expected last argument to be a AHyperType variable"+                )+                (last xs)+            where+                res =+                    foldl AppT (ConT (D.datatypeName info)) (init xs <&> VarT . D.tvName)  childrenTypes :: TypeInfo -> TypeContents childrenTypes info = evalState (childrenTypesH info) mempty@@ -92,13 +110,13 @@         if did             then pure mempty             else-                modify (Lens.contains (tiInstance info) .~ True) *>-                traverse addPat (tiConstructors info ^.. traverse . Lens._3 . traverse . Lens._Right)+                modify (Lens.contains (tiInstance info) .~ True)+                    *> traverse addPat (tiConstructors info ^.. traverse . Lens._3 . traverse . Lens._Right)                     <&> mconcat     where         addPat (FlatEmbed inner) = childrenTypesH inner-        addPat (Node x) = pure mempty { tcChildren = mempty & Lens.contains x .~ True }-        addPat (GenEmbed x) = pure mempty { tcEmbeds = mempty & Lens.contains x .~ True }+        addPat (Node x) = pure mempty{tcChildren = mempty & Lens.contains x .~ True}+        addPat (GenEmbed x) = pure mempty{tcEmbeds = mempty & Lens.contains x .~ True}         addPat (InContainer _ x) = addPat x  unapply :: Type -> (Type, [Type])@@ -106,7 +124,7 @@     go []     where         go as (SigT x _) = go as x-        go as (AppT f a) = go (a:as) f+        go as (AppT f a) = go (a : as) f         go as x = (x, as)  matchType :: Name -> Name -> Type -> Q (Either Type CtrTypePattern)@@ -122,40 +140,38 @@ matchType top var (x `AppT` VarT h)     | h == var && x /= ConT ''GetHyperType =         case unapply x of-        (ConT c, args) | c /= top ->-            do-                inner <- D.reifyDatatype c-                let innerVars = D.datatypeVars inner <&> D.tvName-                let subst =-                        args <> [VarT var]-                        & zip innerVars-                        & Map.fromList-                let makeCons i =-                        D.constructorFields i-                        <&> D.applySubstitution subst-                        & traverse (matchType top var)-                        <&> (D.constructorName i, D.constructorVariant i, )-                cons <- traverse makeCons (D.datatypeCons inner)-                if var `notElem` (D.freeVariablesWellScoped (cons ^.. traverse . Lens._3 . traverse . Lens._Left) <&> D.tvName)-                    then-                        FlatEmbed TypeInfo-                        { tiName = c-                        , tiInstance = x-                        , tiParams = D.datatypeVars inner & init-                        , tiHyperParam = var-                        , tiConstructors = cons-                        } & pure-                    else-                        GenEmbed x & pure-        _ -> GenEmbed x & pure-        <&> Right+            (ConT c, args) | c /= top ->+                do+                    inner <- D.reifyDatatype c+                    let innerVars = D.datatypeVars inner <&> D.tvName+                    let subst =+                            args <> [VarT var]+                                & zip innerVars+                                & Map.fromList+                    let makeCons i =+                            traverse (matchType top var . D.applySubstitution subst) (D.constructorFields i)+                                <&> (D.constructorName i,D.constructorVariant i,)+                    cons <- traverse makeCons (D.datatypeCons inner)+                    if var `notElem` (D.freeVariablesWellScoped (cons ^.. traverse . Lens._3 . traverse . Lens._Left) <&> D.tvName)+                        then+                            FlatEmbed+                                TypeInfo+                                    { tiName = c+                                    , tiInstance = x+                                    , tiParams = D.datatypeVars inner & init+                                    , tiHyperParam = var+                                    , tiConstructors = cons+                                    }+                                & pure+                        else GenEmbed x & pure+            _ -> GenEmbed x & pure+            <&> Right matchType top var x@(AppT f a) =     -- TODO: check if applied over a functor-kinded type.     matchType top var a-    <&>-    \case-    Left{} -> Left x-    Right pat -> InContainer f pat & Right+        <&> \case+            Left{} -> Left x+            Right pat -> InContainer f pat & Right matchType _ _ t = Left t & pure  getVar :: Type -> Maybe Name@@ -174,38 +190,39 @@  makeConstructorVars :: String -> [a] -> [(a, Name)] makeConstructorVars prefix fields =-    [0::Int ..] <&> show <&> (('_':prefix) <>) <&> mkName-    & zip fields+    [0 :: Int ..]+        <&> mkName . (('_' : prefix) <>) . show+        & zip fields  consPat :: Name -> [(a, Name)] -> Q Pat-consPat c vars = conP c (vars <&> snd <&> varP)+consPat c = conP c . (<&> varP . snd)  simplifyContext :: [Pred] -> CxtQ simplifyContext preds =     execStateT (goPreds preds) (mempty :: Set (Name, [Type]), mempty :: Set Pred)-    <&> (^.. Lens._2 . Lens.folded)+        <&> (^.. Lens._2 . Lens.folded)     where-        goPreds ps = ps <&> unapply & traverse_ go+        goPreds = traverse_ (go . unapply)         go (c, [VarT v]) =             -- Work-around reifyInstances returning instances for type variables             -- by not checking.             yep c [VarT v]         go (ConT c, xs) =             Lens.use (Lens._1 . Lens.contains key)-            >>=-            \case-            True -> pure () -- already checked-            False ->-                do-                    Lens._1 . Lens.contains key .= True-                    reifyInstances c xs & lift-                        >>=-                        \case-                        [InstanceD _ context other _] ->-                            D.unifyTypes [other, foldl AppT (ConT c) xs] & lift-                            <&> (`D.applySubstitution` context)-                            >>= goPreds-                        _ -> yep (ConT c) xs+                >>= \case+                    True -> pure () -- already checked+                    False ->+                        do+                            Lens._1 . Lens.contains key .= True+                            reifyInstances c xs+                                & lift+                                >>= \case+                                    [InstanceD _ context other _] ->+                                        D.unifyTypes [other, foldl AppT (ConT c) xs]+                                            & lift+                                            <&> (`D.applySubstitution` context)+                                            >>= goPreds+                                    _ -> yep (ConT c) xs             where                 key = (c, xs)         go (c, xs) = yep c xs@@ -237,30 +254,37 @@         embedBase = "E_" <> niceTypeName <> "_"         pats = tiConstructors info >>= (^. Lens._3)         nodes =-            pats ^.. traverse . Lens._Right >>= nodesForPat & nub-            <&> \t -> (t, mkName (nodeBase <> mkNiceTypeName t))+            pats ^.. traverse . Lens._Right+                >>= nodesForPat+                & nub+                <&> \t -> (t, mkName (nodeBase <> mkNiceTypeName t))         nodesForPat (Node t) = [t]         nodesForPat (InContainer _ pat) = nodesForPat pat         nodesForPat (FlatEmbed x) = tiConstructors x ^.. traverse . Lens._3 . traverse . Lens._Right >>= nodesForPat         nodesForPat _ = []         nodeGadtType (t, n) c = gadtC [n] [] (pure (c `AppT` t))         embeds =-            pats ^.. traverse . Lens._Right >>= embedsForPat & nub-            <&> \t -> (t, mkName (embedBase <> mkNiceTypeName t))+            pats ^.. traverse . Lens._Right+                >>= embedsForPat+                & nub+                <&> \t -> (t, mkName (embedBase <> mkNiceTypeName t))         embedsForPat (GenEmbed t) = [t]         embedsForPat (InContainer _ pat) = embedsForPat pat         embedsForPat (FlatEmbed x) = tiConstructors x ^.. traverse . Lens._3 . traverse . Lens._Right >>= embedsForPat         embedsForPat _ = []         embedGadtType (t, n) c =-            gadtC [n]-            [ bangType (bang noSourceUnpackedness noSourceStrictness)-                [t|HWitness $(pure t) $nodeVar|]-            ] [t|$(pure c) $nodeVar|]+            gadtC+                [n]+                [ bangType+                    (bang noSourceUnpackedness noSourceStrictness)+                    [t|HWitness $(pure t) $nodeVar|]+                ]+                [t|$(pure c) $nodeVar|]         nodeVar = mkName "node" & varT         getWit :: Map Type Name -> Type -> Name         getWit m h =             m ^? Lens.ix h-            & fromMaybe (error ("Cant find witness for " <> show h <> " in " <> show m))+                & fromMaybe (error ("Cant find witness for " <> show h <> " in " <> show m))  mkNiceTypeName :: Type -> String mkNiceTypeName =@@ -268,8 +292,8 @@     where         makeNiceType (ConT x) =             case niceName x of-            n@(c:_) | Char.isAlpha c -> [n]-            _ -> [] -- Skip operators+                n@(c : _) | Char.isAlpha c -> [n]+                _ -> [] -- Skip operators         makeNiceType (AppT x y) = makeNiceType x <> makeNiceType y         makeNiceType (VarT x) = [takeWhile (/= '_') (show x)]         makeNiceType (SigT x _) = makeNiceType x

@@ -1,4 +1,5 @@-{-# LANGUAGE TemplateHaskell, CPP #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE TemplateHaskell #-}  module Hyper.TH.Morph     ( makeHMorph@@ -6,12 +7,12 @@  import qualified Control.Lens as Lens import qualified Data.Map as Map-import           Hyper.Class.Morph (HMorph(..))-import           Hyper.TH.Internal.Utils-import           Language.Haskell.TH+import Hyper.Class.Morph (HMorph (..))+import Hyper.TH.Internal.Utils+import Language.Haskell.TH import qualified Language.Haskell.TH.Datatype as D -import           Hyper.Internal.Prelude+import Hyper.Internal.Prelude  makeHMorph :: Name -> DecsQ makeHMorph typeName = makeTypeInfo typeName >>= makeHMorphForType@@ -20,19 +21,25 @@ makeHMorphForType :: TypeInfo -> DecsQ makeHMorphForType info =     -- TODO: Contexts-    instanceD (pure []) [t|HMorph $(pure src) $(pure dst)|]-    [ D.tySynInstDCompat-        ''MorphConstraint-        (Just [pure (plainTV constraintVar)])-        ([src, dst, VarT constraintVar] <&> pure)-        (simplifyContext morphConstraint <&> toTuple)-    , dataInstD-        (pure []) ''MorphWitness [pure src, pure dst, [t|_|], [t|_|]]-        Nothing (witnesses ^.. traverse . Lens._2) []-    , funD 'morphMap (tiConstructors info <&> mkMorphCon)-    , funD 'morphLiftConstraint liftConstraintClauses-    ]-    <&> (:[])+    instanceD+        (pure [])+        [t|HMorph $(pure src) $(pure dst)|]+        [ D.tySynInstDCompat+            ''MorphConstraint+            (Just [pure (plainTV constraintVar)])+            ([src, dst, VarT constraintVar] <&> pure)+            (simplifyContext morphConstraint <&> toTuple)+        , dataInstD+            (pure [])+            ''MorphWitness+            [pure src, pure dst, [t|_|], [t|_|]]+            Nothing+            (witnesses ^.. traverse . Lens._2)+            []+        , funD 'morphMap (tiConstructors info <&> mkMorphCon)+        , funD 'morphLiftConstraint liftConstraintClauses+        ]+        <&> (: [])     where         (s0, s1) = paramSubsts info         src = D.applySubstitution s0 (tiInstance info)@@ -41,28 +48,33 @@         contents = childrenTypes info         morphConstraint =             (tcChildren contents ^.. Lens.folded <&> appSubsts (VarT constraintVar))-            <> (tcEmbeds contents ^.. Lens.folded <&>-                \x -> ConT ''MorphConstraint `appSubsts` x `AppT` VarT constraintVar)+                <> ( tcEmbeds contents ^.. Lens.folded+                        <&> \x -> ConT ''MorphConstraint `appSubsts` x `AppT` VarT constraintVar+                   )         appSubsts x t = x `AppT` D.applySubstitution s0 t `AppT` D.applySubstitution s1 t         nodeWits =-            tcChildren contents ^.. Lens.folded <&>-            \x ->-            let n = witPrefix <> mkNiceTypeName x & mkName in-            ( x-            , (n, gadtC [n] [] (pure (appSubsts morphWithNessOf x)))-            )+            tcChildren contents ^.. Lens.folded+                <&> \x ->+                    let n = witPrefix <> mkNiceTypeName x & mkName+                    in  ( x+                        , (n, gadtC [n] [] (pure (appSubsts morphWithNessOf x)))+                        )         embedWits =-            tcEmbeds contents ^.. Lens.folded <&>-            \x ->-            let n = witPrefix <> mkNiceTypeName x & mkName in-            ( x-            , ( n-                , gadtC [n]-                    [ bangType (bang noSourceUnpackedness noSourceStrictness)-                        (pure (ConT ''MorphWitness `appSubsts` x `AppT` varA `AppT` varB))-                    ] (pure (morphWithNessOf `AppT` varA `AppT` varB))-              )-            )+            tcEmbeds contents ^.. Lens.folded+                <&> \x ->+                    let n = witPrefix <> mkNiceTypeName x & mkName+                    in  ( x+                        ,+                            ( n+                            , gadtC+                                [n]+                                [ bangType+                                    (bang noSourceUnpackedness noSourceStrictness)+                                    (pure (ConT ''MorphWitness `appSubsts` x `AppT` varA `AppT` varB))+                                ]+                                (pure (morphWithNessOf `AppT` varA `AppT` varB))+                            )+                        )         witnesses = nodeWits <> embedWits & Map.fromList         varA = VarT (mkName "a")         varB = VarT (mkName "b")@@ -71,12 +83,14 @@         liftConstraintClauses             | Map.null witnesses = [clause [] (normalB (lamCaseE [])) []]             | otherwise =-                (nodeWits ^.. traverse . Lens._2 . Lens._1 <&> liftNodeConstraint) <>-                (embedWits ^.. traverse . Lens._2 . Lens._1 <&> liftEmbedConstraint)+                (nodeWits ^.. traverse . Lens._2 . Lens._1 <&> liftNodeConstraint)+                    <> (embedWits ^.. traverse . Lens._2 . Lens._1 <&> liftEmbedConstraint)         liftNodeConstraint n = clause [conP n [], wildP] (normalB [|\x -> x|]) []         liftEmbedConstraint n =-            clause [conP n [varP varW], varP varProxy]-            (normalB [|morphLiftConstraint $(varE varW) $(varE varProxy)|]) []+            clause+                [conP n [varP varW], varP varProxy]+                (normalB [|morphLiftConstraint $(varE varW) $(varE varProxy)|])+                []         varW = mkName "w"         varProxy = mkName "p"         mkMorphCon con =@@ -94,8 +108,9 @@     )     where         cVars =-            [i ..] <&> show <&> ('x':) <&> mkName-            & take (length fields)+            [i ..]+                <&> mkName . ('x' :) . show+                & take (length fields)         f = varE varF         bodyFor Left{} v = varE v         bodyFor (Right x) v = [|$(bodyForPat x) $(varE v)|]@@ -103,10 +118,11 @@         bodyForPat (InContainer _ pat) = [|fmap $(bodyForPat pat)|]         bodyForPat (FlatEmbed x) =             lamCaseE-            (tiConstructors x-                <&> morphCon (i + length cVars) witnesses-                <&> \(p, b) -> match p b []-            )+                ( tiConstructors x+                    <&> uncurry match+                        . morphCon (i + length cVars) witnesses+                        ?? []+                )         bodyForPat (GenEmbed t) = [|morphMap ($f . $(conE (witnesses ^?! Lens.ix t . Lens._1)))|]  type MorphSubsts = (Map Name Type, Map Name Type)

@@ -1,19 +1,19 @@-{-# LANGUAGE TemplateHaskell, EmptyCase #-}+{-# LANGUAGE EmptyCase #-}+{-# LANGUAGE TemplateHaskell #-}  -- | Generate 'HNodes' instances via @TemplateHaskell@- module Hyper.TH.Nodes     ( makeHNodes     ) where  import qualified Control.Lens as Lens-import           GHC.Generics (V1)-import           Hyper.Class.Nodes (HNodes(..), HWitness(..))-import           Hyper.TH.Internal.Utils-import           Language.Haskell.TH+import GHC.Generics (V1)+import Hyper.Class.Nodes (HNodes (..), HWitness (..))+import Hyper.TH.Internal.Utils+import Language.Haskell.TH import qualified Language.Haskell.TH.Datatype as D -import           Hyper.Internal.Prelude+import Hyper.Internal.Prelude  -- | Generate a 'HNodes' instance makeHNodes :: Name -> DecsQ@@ -21,7 +21,9 @@  makeHNodesForType :: TypeInfo -> DecsQ makeHNodesForType info =-    [ instanceD (simplifyContext (makeContext info)) [t|HNodes $(pure (tiInstance info))|]+    [ instanceD+        (simplifyContext (makeContext info))+        [t|HNodes $(pure (tiInstance info))|]         [ D.tySynInstDCompat             ''HNodesConstraint             (Just [pure (plainTV constraintVar)])@@ -31,16 +33,22 @@         , InlineP 'hLiftConstraint Inline FunLike AllPhases & PragmaD & pure         , funD 'hLiftConstraint (makeHLiftConstraints wit)         ]-    ] <> witDecs-    & sequenceA+    ]+        <> witDecs+        & sequenceA     where         (witType, witDecs)             | null nodeOfCons = ([t|V1|], [])             | otherwise =                 ( tiParams info <&> varT . D.tvName & foldl appT (conT witTypeName)-                , [dataD (pure []) witTypeName-                    (tiParams info <> [plainTV (mkName "node")])-                    Nothing (nodeOfCons <&> (witType >>=)) []+                ,+                    [ dataD+                        (pure [])+                        witTypeName+                        (tiParams info <> [plainTV (mkName "node")])+                        Nothing+                        (nodeOfCons <&> (witType >>=))+                        []                     ]                 )             where@@ -51,9 +59,9 @@         contents = childrenTypes info         nodesConstraint =             (tcChildren contents ^.. Lens.folded <&> (c `appT`) . pure)-            <> (tcEmbeds contents ^.. Lens.folded <&> \x -> [t|HNodesConstraint $(pure x) $c|])-            <> (tcOthers contents ^.. Lens.folded <&> pure)-            & sequenceA+                <> (tcEmbeds contents ^.. Lens.folded <&> \x -> [t|HNodesConstraint $(pure x) $c|])+                <> (tcOthers contents ^.. Lens.folded <&> pure)+                & sequenceA  makeContext :: TypeInfo -> [Pred] makeContext info =@@ -61,17 +69,20 @@     where         ctxForPat (InContainer _ pat) = ctxForPat pat         ctxForPat (GenEmbed t) = [ConT ''HNodes `AppT` t]+        ctxForPat (FlatEmbed t) = makeContext t         ctxForPat _ = []  makeHLiftConstraints :: NodeWitnesses -> [Q Clause] makeHLiftConstraints wit-    | null clauses = [clause [] (normalB [|\case|]) []]+    | null clauses = [clause [] (normalB [|\case {}|]) []]     | otherwise = clauses     where         clauses = (nodeWitCtrs wit <&> liftNode) <> (embedWitCtrs wit <&> liftEmbed)         liftNode x = clause [conP 'HWitness [conP x []]] (normalB [|\_ r -> r|]) []         liftEmbed x =-            clause [conP 'HWitness [conP x [varP witVar]]]-            (normalB [|hLiftConstraint $(varE witVar)|]) []+            clause+                [conP 'HWitness [conP x [varP witVar]]]+                (normalB [|hLiftConstraint $(varE witVar)|])+                []         witVar :: Name         witVar = mkName "witness"

@@ -1,18 +1,17 @@ {-# LANGUAGE TemplateHaskell #-}  -- | Generate 'HPointed' instances via @TemplateHaskell@- module Hyper.TH.Pointed     ( makeHPointed     ) where  import qualified Control.Lens as Lens-import           Hyper.Class.Pointed (HPointed(..))-import           Hyper.TH.Internal.Utils-import           Language.Haskell.TH-import           Language.Haskell.TH.Datatype (ConstructorVariant)+import Hyper.Class.Pointed (HPointed (..))+import Hyper.TH.Internal.Utils+import Language.Haskell.TH+import Language.Haskell.TH.Datatype (ConstructorVariant) -import           Hyper.Internal.Prelude+import Hyper.Internal.Prelude  -- | Generate a 'HPointed' instance makeHPointed :: Name -> DecsQ@@ -23,22 +22,24 @@     do         cons <-             case tiConstructors info of-            [x] -> pure x-            _ -> fail "makeHPointed only supports types with a single constructor"-        instanceD (makeContext info >>= simplifyContext) [t|HPointed $(pure (tiInstance info))|]+                [x] -> pure x+                _ -> fail "makeHPointed only supports types with a single constructor"+        instanceD+            (makeContext info >>= simplifyContext)+            [t|HPointed $(pure (tiInstance info))|]             [ InlineP 'hpure Inline FunLike AllPhases & PragmaD & pure             , funD 'hpure [makeHPureCtr info cons]             ]-    <&> (:[])+        <&> (: [])  makeContext :: TypeInfo -> Q [Pred] makeContext info =     tiConstructors info >>= (^. Lens._3) & traverse ctxFor <&> mconcat     where         ctxFor (Right x) = ctxForPat x-        ctxFor (Left x) = [t|Monoid $(pure x)|] <&> (:[])+        ctxFor (Left x) = [t|Monoid $(pure x)|] <&> (: [])         ctxForPat (InContainer t pat) = (:) <$> [t|Applicative $(pure t)|] <*> ctxForPat pat-        ctxForPat (GenEmbed t) = [t|HPointed $(pure t)|] <&> (:[])+        ctxForPat (GenEmbed t) = [t|HPointed $(pure t)|] <&> (: [])         ctxForPat (FlatEmbed t) = makeContext t         ctxForPat _ = pure [] @@ -52,8 +53,8 @@         bodyForPat (Node t) = [|$f $(nodeWit wit t)|]         bodyForPat (FlatEmbed inner) =             case tiConstructors inner of-            [(iName, _, iFields)] -> iFields <&> bodyFor & foldl appE (conE iName)-            _ -> fail "makeHPointed only supports embedded types with a single constructor"+                [(iName, _, iFields)] -> iFields <&> bodyFor & foldl appE (conE iName)+                _ -> fail "makeHPointed only supports embedded types with a single constructor"         bodyForPat (GenEmbed t) = [|hpure ($f . $(embedWit wit t))|]         bodyForPat (InContainer _ pat) = [|pure $(bodyForPat pat)|]         varF = mkName "_f"

@@ -1,7 +1,6 @@ {-# LANGUAGE TemplateHaskell #-}  -- | Generate 'HTraversable' and related instances via @TemplateHaskell@- module Hyper.TH.Traversable     ( makeHTraversable     , makeHTraversableAndFoldable@@ -10,16 +9,16 @@     ) where  import qualified Control.Lens as Lens-import           Hyper.Class.Traversable (HTraversable(..), ContainedH(..))-import           Hyper.TH.Apply (makeHApplicativeBases)-import           Hyper.TH.Foldable (makeHFoldable)-import           Hyper.TH.Functor (makeHFunctor)-import           Hyper.TH.Internal.Utils-import           Hyper.TH.Nodes (makeHNodes)-import           Language.Haskell.TH-import           Language.Haskell.TH.Datatype (ConstructorVariant)+import Hyper.Class.Traversable (ContainedH (..), HTraversable (..))+import Hyper.TH.Apply (makeHApplicativeBases)+import Hyper.TH.Foldable (makeHFoldable)+import Hyper.TH.Functor (makeHFunctor)+import Hyper.TH.Internal.Utils+import Hyper.TH.Nodes (makeHNodes)+import Language.Haskell.TH+import Language.Haskell.TH.Datatype (ConstructorVariant) -import           Hyper.Internal.Prelude+import Hyper.Internal.Prelude  -- | Generate 'HTraversable' and 'Hyper.Class.Apply.HApply' instances along with all of their base classes: -- 'Hyper.Class.Foldable.HFoldable', 'Hyper.Class.Functor.HFunctor',@@ -27,27 +26,30 @@ makeHTraversableApplyAndBases :: Name -> DecsQ makeHTraversableApplyAndBases x =     sequenceA-    [ makeHApplicativeBases x-    , makeHTraversableAndFoldable x-    ] <&> concat+        [ makeHApplicativeBases x+        , makeHTraversableAndFoldable x+        ]+        <&> concat  -- | Generate a 'HTraversable' instance along with the instance of its base classes: -- 'Hyper.Class.Foldable.HFoldable', 'Hyper.Class.Functor.HFunctor', and 'Hyper.Class.Nodes.HNodes'. makeHTraversableAndBases :: Name -> DecsQ makeHTraversableAndBases x =     sequenceA-    [ makeHNodes x-    , makeHFunctor x-    , makeHTraversableAndFoldable x-    ] <&> concat+        [ makeHNodes x+        , makeHFunctor x+        , makeHTraversableAndFoldable x+        ]+        <&> concat  -- | Generate 'HTraversable' and 'Hyper.Class.Foldable.HFoldable' instances makeHTraversableAndFoldable :: Name -> DecsQ makeHTraversableAndFoldable x =     sequenceA-    [ makeHFoldable x-    , makeHTraversable x-    ] <&> concat+        [ makeHFoldable x+        , makeHTraversable x+        ]+        <&> concat  -- | Generate a 'HTraversable' instance makeHTraversable :: Name -> DecsQ@@ -55,19 +57,22 @@  makeHTraversableForType :: TypeInfo -> DecsQ makeHTraversableForType info =-    instanceD (makeContext info >>= simplifyContext) [t|HTraversable $(pure (tiInstance info))|]-    [ InlineP 'hsequence Inline FunLike AllPhases & PragmaD & pure-    , funD 'hsequence (tiConstructors info <&> makeCons)-    ]-    <&> (:[])+    instanceD+        (makeContext info >>= simplifyContext)+        [t|HTraversable $(pure (tiInstance info))|]+        [ InlineP 'hsequence Inline FunLike AllPhases & PragmaD & pure+        , funD 'hsequence (tiConstructors info <&> makeCons)+        ]+        <&> (: [])  makeContext :: TypeInfo -> Q [Pred] makeContext info =     tiConstructors info ^.. traverse . Lens._3 . traverse . Lens._Right-    & traverse ctxForPat <&> mconcat+        & traverse ctxForPat+        <&> mconcat     where         ctxForPat (InContainer t pat) = (:) <$> [t|Traversable $(pure t)|] <*> ctxForPat pat-        ctxForPat (GenEmbed t) = [t|HTraversable $(pure t)|] <&> (:[])+        ctxForPat (GenEmbed t) = [t|HTraversable $(pure t)|] <&> (: [])         ctxForPat (FlatEmbed t) = makeContext t         ctxForPat _ = pure [] @@ -77,9 +82,10 @@     clause [consPat cName consVars] body []     where         body =-            consVars <&> f-            & applicativeStyle (conE cName)-            & normalB+            consVars+                <&> f+                & applicativeStyle (conE cName)+                & normalB         consVars = makeConstructorVars "x" cFields         f (pat, name) = bodyFor pat `appE` varE name         bodyFor (Right x) = bodyForPat x

@@ -1,13 +1,12 @@ {-# LANGUAGE TemplateHaskell #-}  -- | Generate 'ZipMatch' instances via @TemplateHaskell@- module Hyper.TH.ZipMatch     ( makeZipMatch     ) where  import Control.Lens (both)-import Hyper.Class.ZipMatch (ZipMatch(..))+import Hyper.Class.ZipMatch (ZipMatch (..)) import Hyper.TH.Internal.Utils import Language.Haskell.TH import Language.Haskell.TH.Datatype (ConstructorVariant)@@ -27,12 +26,11 @@             [ InlineP 'zipMatch Inline FunLike AllPhases & PragmaD & pure             , funD 'zipMatch ((ctrs <&> ccClause) <> [tailClause])             ]-            <&> (:[])+            <&> (: [])     where         tailClause = clause [wildP, wildP] (normalB [|Nothing|]) [] -data CtrCase =-    CtrCase+data CtrCase = CtrCase     { ccClause :: Q Clause     , ccContext :: [Q Pred]     }@@ -40,14 +38,15 @@ makeZipMatchCtr :: (Name, ConstructorVariant, [Either Type CtrTypePattern]) -> CtrCase makeZipMatchCtr (cName, _, cFields) =     CtrCase-    { ccClause = clause [con fst, con snd] body []-    , ccContext = fieldParts >>= zmfContext-    }+        { ccClause = clause [con fst, con snd] body []+        , ccContext = fieldParts >>= zmfContext+        }     where-        con f = conP cName (cVars <&> f <&> varP)+        con f = conP cName (cVars <&> varP . f)         cVars =-            [0::Int ..] <&> show <&> (\n -> (mkName ('x':n), mkName ('y':n)))-            & take (length cFields)+            [0 :: Int ..]+                <&> (\n -> (mkName ('x' : n), mkName ('y' : n))) . show+                & take (length cFields)         body             | null checks = normalB bodyExp             | otherwise = guardedB [(,) <$> normalG (foldl1 mkAnd checks) <*> bodyExp]@@ -57,25 +56,25 @@         bodyExp = applicativeStyle (conE cName) (fieldParts <&> zmfResult)         field (x, y) (Right Node{}) =             ZipMatchField-            { zmfResult = [|Just ($x :*: $y)|]-            , zmfConds = []-            , zmfContext = []-            }+                { zmfResult = [|Just ($x :*: $y)|]+                , zmfConds = []+                , zmfContext = []+                }         field (x, y) (Right (GenEmbed t)) = embed t x y         field (x, y) (Right (FlatEmbed t)) = embed (tiInstance t) x y         field _ (Right InContainer{}) = error "TODO"         field (x, y) (Left t) =             ZipMatchField-            { zmfResult = [|Just $x|]-            , zmfConds =  [[|$x == $y|]]-            , zmfContext = [[t|Eq $(pure t)|]]-            }+                { zmfResult = [|Just $x|]+                , zmfConds = [[|$x == $y|]]+                , zmfContext = [[t|Eq $(pure t)|]]+                }         embed t x y =             ZipMatchField-            { zmfResult = [|zipMatch $x $y|]-            , zmfConds = []-            , zmfContext = [[t|ZipMatch $(pure t)|]]-            }+                { zmfResult = [|zipMatch $x $y|]+                , zmfConds = []+                , zmfContext = [[t|ZipMatch $(pure t)|]]+                }  data ZipMatchField = ZipMatchField     { zmfResult :: Q Exp

@@ -3,11 +3,12 @@ -- This infinite definition is expressible using the 'AHyperType' 'Data.Kind.Kind' for hypertypes. -- -- For more information see the [README](https://github.com/lamdu/hypertypes/blob/master/README.md).- module Hyper.Type     ( HyperType-    , AHyperType(..), GetHyperType-    , type (#), type (:#)+    , AHyperType (..)+    , GetHyperType+    , type (#)+    , type (:#)     , asHyper     ) where 

@@ -1,64 +0,0 @@-{-# LANGUAGE FlexibleInstances, UndecidableInstances, TemplateHaskell #-}--module Hyper.Type.AST.App-    ( App(..), appFunc, appArg, W_App(..), MorphWitness(..)-    ) where--import Hyper-import Hyper.Class.Optic (HSubset(..), HSubset')-import Hyper.Infer-import Hyper.Type.AST.FuncType-import Hyper.Unify (UnifyGen, unify)-import Hyper.Unify.New (newTerm, newUnbound)-import Text.PrettyPrint ((<+>))-import Text.PrettyPrint.HughesPJClass (Pretty(..), maybeParens)--import Hyper.Internal.Prelude---- | A term for function applications.------ @App expr@s express function applications of @expr@s.------ Apart from the data type, an 'Infer' instance is also provided.-data App expr h = App-    { _appFunc :: h :# expr-    , _appArg :: h :# expr-    } deriving Generic--makeLenses ''App-makeZipMatch ''App-makeHContext ''App-makeHMorph ''App-makeHTraversableApplyAndBases ''App-makeCommonInstances [''App]--instance RNodes e => RNodes (App e)-instance (c (App e), Recursively c e) => Recursively c (App e)-instance RTraversable e => RTraversable (App e)--instance Pretty (h :# expr) => Pretty (App expr h) where-    pPrintPrec lvl p (App f x) =-        pPrintPrec lvl 10 f <+>-        pPrintPrec lvl 11 x-        & maybeParens (p > 10)--type instance InferOf (App e) = ANode (TypeOf e)--instance-    ( Infer m expr-    , HasInferredType expr-    , HSubset' (TypeOf expr) (FuncType (TypeOf expr))-    , UnifyGen m (TypeOf expr)-    ) =>-    Infer m (App expr) where--    {-# INLINE inferBody #-}-    inferBody (App func arg) =-        do-            InferredChild argI argR <- inferChild arg-            InferredChild funcI funcR <- inferChild func-            funcRes <- newUnbound-            (App funcI argI, MkANode funcRes) <$-                (newTerm (hSubset # FuncType (argR ^# l) funcRes) >>= unify (funcR ^# l))-        where-            l = inferredType (Proxy @expr)

@@ -1,38 +0,0 @@-{-# LANGUAGE UndecidableInstances, TemplateHaskell #-}--module Hyper.Type.AST.FuncType-    ( FuncType(..), funcIn, funcOut, W_FuncType(..), MorphWitness(..)-    ) where--import           Generics.Constraints (makeDerivings, makeInstances)-import           Hyper-import           Text.PrettyPrint ((<+>))-import qualified Text.PrettyPrint as Pretty-import           Text.PrettyPrint.HughesPJClass (Pretty(..), maybeParens)-import           Text.Show.Combinators ((@|), showCon)--import           Hyper.Internal.Prelude---- | A term for the types of functions. Analogues to @(->)@ in Haskell.------ @FuncType typ@s express types of functions of @typ@.-data FuncType typ h = FuncType-    { _funcIn  :: h :# typ-    , _funcOut :: h :# typ-    } deriving Generic--makeLenses ''FuncType-makeZipMatch ''FuncType-makeHContext ''FuncType-makeHMorph ''FuncType-makeHTraversableApplyAndBases ''FuncType-makeDerivings [''Eq, ''Ord] [''FuncType]-makeInstances [''Binary, ''NFData] [''FuncType]--instance Pretty (h :# typ) => Pretty (FuncType typ h) where-    pPrintPrec lvl p (FuncType i o) =-        pPrintPrec lvl 11 i <+> Pretty.text "->" <+> pPrintPrec lvl 10 o-        & maybeParens (p > 10)--instance Show (h :# typ) => Show (FuncType typ h) where-    showsPrec p (FuncType i o) = (showCon "FuncType" @| i @| o) p

@@ -1,67 +0,0 @@-{-# LANGUAGE TemplateHaskell, FlexibleInstances, UndecidableInstances #-}--module Hyper.Type.AST.Lam-    ( Lam(..), lamIn, lamOut, W_Lam(..), MorphWitness(..)-    ) where--import           Generics.Constraints (Constraints)-import           Hyper-import           Hyper.Class.Optic (HSubset(..), HSubset')-import           Hyper.Infer-import           Hyper.Type.AST.FuncType-import           Hyper.Unify (UnifyGen, UVarOf)-import           Hyper.Unify.New (newUnbound, newTerm)-import qualified Text.PrettyPrint as P-import           Text.PrettyPrint.HughesPJClass (Pretty(..), maybeParens)--import           Hyper.Internal.Prelude---- | A term for lambda abstractions.------ @Lam v expr@s express lambda abstractions with @v@s as variable names and @expr@s for bodies.------ Apart from the data type, an 'Infer' instance is also provided.-data Lam v expr h = Lam-    { _lamIn :: v-    , _lamOut :: h :# expr-    } deriving Generic--makeLenses ''Lam-makeCommonInstances [''Lam]-makeHTraversableApplyAndBases ''Lam-makeZipMatch ''Lam-makeHContext ''Lam-makeHMorph ''Lam--instance RNodes t => RNodes (Lam v t)-instance (c (Lam v t), Recursively c t) => Recursively c (Lam v t)-instance RTraversable t => RTraversable (Lam v t)--instance-    Constraints (Lam v expr h) Pretty =>-    Pretty (Lam v expr h) where-    pPrintPrec lvl p (Lam i o) =-        (P.text "λ" <> pPrintPrec lvl 0 i)-        P.<+> P.text "→" P.<+> pPrintPrec lvl 0 o-        & maybeParens (p > 0)--type instance InferOf (Lam _ t) = ANode (TypeOf t)--instance-    ( Infer m t-    , UnifyGen m (TypeOf t)-    , HSubset' (TypeOf t) (FuncType (TypeOf t))-    , HasInferredType t-    , LocalScopeType v (UVarOf m # TypeOf t) m-    ) =>-    Infer m (Lam v t) where--    {-# INLINE inferBody #-}-    inferBody (Lam p r) =-        do-            varType <- newUnbound-            InferredChild rI rR <- inferChild r & localScopeType p varType-            hSubset # FuncType varType (rR ^# inferredType (Proxy @t))-                & newTerm-                <&> MkANode-                <&> (Lam p rI,)

@@ -1,68 +0,0 @@-{-# LANGUAGE TemplateHaskell, UndecidableInstances, FlexibleInstances #-}--module Hyper.Type.AST.Let-    ( Let(..), letVar, letEquals, letIn, W_Let(..), MorphWitness(..)-    ) where--import           Generics.Constraints (Constraints)-import           Hyper-import           Hyper.Class.Unify (UnifyGen, UVarOf)-import           Hyper.Infer-import           Hyper.Unify.Generalize (GTerm, generalize)-import           Text.PrettyPrint (($+$), (<+>))-import qualified Text.PrettyPrint as Pretty-import           Text.PrettyPrint.HughesPJClass (Pretty(..), maybeParens)--import           Hyper.Internal.Prelude---- | A term for let-expressions with let-generalization.------ @Let v expr@s express let-expressions with @v@s as variable names and @expr@s for terms.------ Apart from the data type, an 'Infer' instance is also provided.-data Let v expr h = Let-    { _letVar :: v-    , _letEquals :: h :# expr-    , _letIn :: h :# expr-    } deriving (Generic)--makeLenses ''Let-makeCommonInstances [''Let]-makeHTraversableApplyAndBases ''Let-makeZipMatch ''Let-makeHContext ''Let-makeHMorph ''Let--instance-    Constraints (Let v expr h) Pretty =>-    Pretty (Let v expr h) where-    pPrintPrec lvl p (Let v e i) =-        Pretty.text "let" <+> pPrintPrec lvl 0 v <+> Pretty.text "="-        <+> pPrintPrec lvl 0 e-        $+$ pPrintPrec lvl 0 i-        & maybeParens (p > 0)--type instance InferOf (Let _ e) = InferOf e--instance-    ( MonadScopeLevel m-    , LocalScopeType v (GTerm (UVarOf m) # TypeOf expr) m-    , UnifyGen m (TypeOf expr)-    , HasInferredType expr-    , HNodesConstraint (InferOf expr) (UnifyGen m)-    , HTraversable (InferOf expr)-    , Infer m expr-    ) =>-    Infer m (Let v expr) where--    inferBody (Let v e i) =-        do-            (eI, eG) <--                do-                    InferredChild eI eR <- inferChild e-                    generalize (eR ^# inferredType (Proxy @expr))-                        <&> (eI ,)-                & localLevel-            inferChild i-                & localScopeType v eG-                <&> \(InferredChild iI iR) -> (Let v eI iI, iR)

@@ -1,40 +0,0 @@-{-# LANGUAGE TemplateHaskell, FlexibleInstances, UndecidableInstances #-}--module Hyper.Type.AST.Map-    ( TermMap(..), _TermMap, W_TermMap(..), MorphWitness(..)-    ) where--import qualified Control.Lens as Lens-import qualified Data.Map as Map-import           Hyper-import           Hyper.Class.ZipMatch (ZipMatch(..))--import           Hyper.Internal.Prelude---- | A mapping of keys to terms.------ Apart from the data type, a 'ZipMatch' instance is also provided.-newtype TermMap h expr f = TermMap (Map h (f :# expr))-    deriving stock Generic--makePrisms ''TermMap-makeCommonInstances [''TermMap]-makeHTraversableApplyAndBases ''TermMap-makeHMorph ''TermMap--instance Eq h => ZipMatch (TermMap h expr) where-    {-# INLINE zipMatch #-}-    zipMatch (TermMap x) (TermMap y)-        | Map.size x /= Map.size y = Nothing-        | otherwise =-            zipMatchList (x ^@.. Lens.itraversed) (y ^@.. Lens.itraversed)-            <&> traverse . Lens._2 %~ uncurry (:*:)-            <&> TermMap . Map.fromAscList--{-# INLINE zipMatchList #-}-zipMatchList :: Eq k => [(k, a)] -> [(k, b)] -> Maybe [(k, (a, b))]-zipMatchList [] [] = Just []-zipMatchList ((k0, v0) : xs) ((k1, v1) : ys)-    | k0 == k1 =-        zipMatchList xs ys <&> ((k0, (v0, v1)) :)-zipMatchList _ _ = Nothing

@@ -1,361 +0,0 @@--- | Nominal (named) types declaration, instantiation, construction, and access.--{-# LANGUAGE FlexibleInstances, UndecidableInstances #-}-{-# LANGUAGE FlexibleContexts, TemplateHaskell, EmptyCase #-}--module Hyper.Type.AST.Nominal-    ( NominalDecl(..), nParams, nScheme, W_NominalDecl(..)-    , NominalInst(..), nId, nArgs-    , ToNom(..), tnId, tnVal, W_ToNom(..)-    , FromNom(..), _FromNom--    , HasNominalInst(..)-    , NomVarTypes-    , MonadNominals(..)-    , LoadedNominalDecl, loadNominalDecl-    ) where--import           Control.Applicative (Alternative(..))-import           Control.Lens (Prism')-import qualified Control.Lens as Lens-import           Control.Monad.Trans.Writer (execWriterT)-import           Generics.Constraints (Constraints)-import           Hyper-import           Hyper.Class.Context (HContext(..))-import           Hyper.Class.Optic-import           Hyper.Class.Traversable (ContainedH(..))-import           Hyper.Class.ZipMatch (ZipMatch(..))-import           Hyper.Infer-import           Hyper.Recurse-import           Hyper.Type.AST.FuncType (FuncType(..))-import           Hyper.Type.AST.Map (TermMap(..), _TermMap)-import           Hyper.Type.AST.Scheme-import           Hyper.Unify-import           Hyper.Unify.Generalize (GTerm(..), _GMono, instantiateWith, instantiateForAll)-import           Hyper.Unify.New (newTerm)-import           Hyper.Unify.QuantifiedVar (HasQuantifiedVar(..), OrdQVar)-import           Hyper.Unify.Term (UTerm(..))-import qualified Text.PrettyPrint as P-import           Text.PrettyPrint.HughesPJClass (Pretty(..), maybeParens)--import           Hyper.Internal.Prelude--type family NomVarTypes (t :: HyperType) :: HyperType---- | A declaration of a nominal type.-data NominalDecl typ h = NominalDecl-    { _nParams :: NomVarTypes typ # QVars-    , _nScheme :: Scheme (NomVarTypes typ) typ h-    } deriving Generic---- | An instantiation of a nominal type-data NominalInst nomId varTypes h = NominalInst-    { _nId :: nomId-    , _nArgs :: varTypes # QVarInstances (GetHyperType h)-    } deriving Generic---- | Nominal data constructor.------ Wrap content with a data constructor--- (analogues to a data constructor of a Haskell `newtype`'s).------ Introduces the nominal's foralled type variables into the value's scope.-data ToNom nomId term h = ToNom-    { _tnId :: nomId-    , _tnVal :: h :# term-    } deriving Generic---- | Access the data in a nominally typed value.------ Analogues to a getter of a Haskell `newtype`.-newtype FromNom nomId (term :: HyperType) (h :: AHyperType) = FromNom nomId-    deriving newtype (Eq, Ord, Binary, NFData)-    deriving stock (Show, Generic)---- | A nominal declaration loaded into scope in an inference monad.-data LoadedNominalDecl typ v = LoadedNominalDecl-    { _lnParams :: NomVarTypes typ # QVarInstances (GetHyperType v)-    , _lnForalls :: NomVarTypes typ # QVarInstances (GetHyperType v)-    , _lnType :: GTerm (GetHyperType v) # typ-    } deriving Generic--makeLenses ''NominalDecl-makeLenses ''NominalInst-makeLenses ''ToNom-makePrisms ''FromNom-makeCommonInstances [''NominalDecl, ''NominalInst, ''ToNom, ''LoadedNominalDecl]-makeHTraversableAndBases ''NominalDecl-makeHTraversableApplyAndBases ''ToNom-makeHTraversableApplyAndBases ''FromNom-makeHMorph ''ToNom-makeZipMatch ''ToNom-makeZipMatch ''FromNom-makeHContext ''ToNom-makeHContext ''FromNom--instance HNodes v => HNodes (NominalInst n v) where-    type HNodesConstraint (NominalInst n v) c = HNodesConstraint v c-    type HWitnessType (NominalInst n v) = HWitnessType v-    {-# INLINE hLiftConstraint #-}-    hLiftConstraint (HWitness w) = hLiftConstraint @v (HWitness w)--instance HFunctor v => HFunctor (NominalInst n v) where-    {-# INLINE hmap #-}-    hmap f = nArgs %~ hmap (\(HWitness w) -> _QVarInstances . Lens.mapped %~ f (HWitness w))--instance HFoldable v => HFoldable (NominalInst n v) where-    {-# INLINE hfoldMap #-}-    hfoldMap f =-        hfoldMap (\(HWitness w) -> foldMap (f (HWitness w)) . (^. _QVarInstances)) . (^. nArgs)--instance HTraversable v => HTraversable (NominalInst n v) where-    {-# INLINE hsequence #-}-    hsequence (NominalInst n v) =-        htraverse (const (_QVarInstances (traverse runContainedH))) v-        <&> NominalInst n--instance-    ( Eq nomId-    , ZipMatch varTypes-    , HTraversable varTypes-    , HNodesConstraint varTypes ZipMatch-    , HNodesConstraint varTypes OrdQVar-    ) =>-    ZipMatch (NominalInst nomId varTypes) where--    {-# INLINE zipMatch #-}-    zipMatch (NominalInst xId x) (NominalInst yId y)-        | xId /= yId = Nothing-        | otherwise =-            zipMatch x y-            >>= htraverse-                ( Proxy @ZipMatch #*# Proxy @OrdQVar #>-                    \(QVarInstances c0 :*: QVarInstances c1) ->-                    zipMatch (TermMap c0) (TermMap c1)-                    <&> (^. _TermMap)-                    <&> QVarInstances-                )-            <&> NominalInst xId--instance-    ( HFunctor varTypes-    , HContext varTypes-    , HNodesConstraint varTypes OrdQVar-    ) => HContext (NominalInst nomId varTypes) where-    hcontext (NominalInst n args) =-        hcontext args-        & hmap-            ( Proxy @OrdQVar #>-                \(HFunc c :*: x) ->-                x & _QVarInstances . Lens.imapped %@~-                \k v ->-                HFunc-                ( \newV ->-                    x-                    & _QVarInstances . Lens.at k ?~ newV-                    & c & getConst & NominalInst n-                    & Const-                ) :*: v-            )-        & NominalInst n--instance Constraints (ToNom nomId term h) Pretty => Pretty (ToNom nomId term h) where-    pPrintPrec lvl p (ToNom nomId term) =-        (pPrint nomId <> P.text "#") P.<+> pPrintPrec lvl 11 term-        & maybeParens (p > 10)--class    (Pretty (QVar h), Pretty (outer :# h)) => PrettyConstraints outer h-instance (Pretty (QVar h), Pretty (outer :# h)) => PrettyConstraints outer h--instance-    ( Pretty nomId-    , HApply varTypes, HFoldable varTypes-    , HNodesConstraint varTypes (PrettyConstraints h)-    ) =>-    Pretty (NominalInst nomId varTypes h) where--    pPrint (NominalInst n vars) =-        pPrint n <>-        joinArgs-        (hfoldMap (Proxy @(PrettyConstraints h) #> mkArgs) vars)-        where-            joinArgs [] = mempty-            joinArgs xs = P.text "[" <> P.sep (P.punctuate (P.text ",") xs) <> P.text "]"-            mkArgs (QVarInstances m) =-                m ^@.. Lens.itraversed <&>-                \(h, v) ->-                (pPrint h <> P.text ":") P.<+> pPrint v--{-# ANN module "HLint: ignore Use camelCase" #-}-data W_LoadedNominalDecl t n where-    E_LoadedNominalDecl_Body :: HRecWitness t n -> W_LoadedNominalDecl t n-    E_LoadedNominalDecl_NomVarTypes :: HWitness (NomVarTypes t) n -> W_LoadedNominalDecl t n--instance (RNodes t, HNodes (NomVarTypes t)) => HNodes (LoadedNominalDecl t) where-    type HNodesConstraint (LoadedNominalDecl t) c =-        ( HNodesConstraint (NomVarTypes t) c-        , c t-        , Recursive c-        )-    type HWitnessType (LoadedNominalDecl t) = W_LoadedNominalDecl t-    {-# INLINE hLiftConstraint #-}-    hLiftConstraint (HWitness (E_LoadedNominalDecl_Body w)) = hLiftConstraint @(HFlip GTerm _) (HWitness w)-    hLiftConstraint (HWitness (E_LoadedNominalDecl_NomVarTypes w)) = hLiftConstraint w--instance-    (Recursively HFunctor typ, HFunctor (NomVarTypes typ)) =>-    HFunctor (LoadedNominalDecl typ) where-    {-# INLINE hmap #-}-    hmap f (LoadedNominalDecl mp mf t) =-        LoadedNominalDecl (onMap mp) (onMap mf)-        (t & hflipped %~ hmap (\(HWitness w) -> f (HWitness (E_LoadedNominalDecl_Body w))))-        where-            onMap = hmap (\w -> _QVarInstances . Lens.mapped %~ f (HWitness (E_LoadedNominalDecl_NomVarTypes w)))--instance-    (Recursively HFoldable typ, HFoldable (NomVarTypes typ)) =>-    HFoldable (LoadedNominalDecl typ) where-    {-# INLINE hfoldMap #-}-    hfoldMap f (LoadedNominalDecl mp mf t) =-        onMap mp <> onMap mf <>-        hfoldMap (\(HWitness w) -> f (HWitness (E_LoadedNominalDecl_Body w))) (_HFlip # t)-        where-            onMap =-                hfoldMap (\w -> foldMap (f (HWitness (E_LoadedNominalDecl_NomVarTypes w)))-                . (^. _QVarInstances))--instance-    (RTraversable typ, HTraversable (NomVarTypes typ)) =>-    HTraversable (LoadedNominalDecl typ) where-    {-# INLINE hsequence #-}-    hsequence (LoadedNominalDecl p f t) =-        LoadedNominalDecl-        <$> onMap p-        <*> onMap f-        <*> hflipped hsequence t-        where-            onMap = htraverse (const ((_QVarInstances . traverse) runContainedH))--{-# INLINE loadBody #-}-loadBody ::-    ( UnifyGen m typ-    , HNodeLens varTypes typ-    , Ord (QVar typ)-    ) =>-    varTypes # QVarInstances (UVarOf m) ->-    varTypes # QVarInstances (UVarOf m) ->-    typ # GTerm (UVarOf m) ->-    m (GTerm (UVarOf m) # typ)-loadBody params foralls x =-    case x ^? quantifiedVar >>= get of-    Just r -> GPoly r & pure-    Nothing ->-        case htraverse (const (^? _GMono)) x of-        Just xm -> newTerm xm <&> GMono-        Nothing -> GBody x & pure-    where-        get v =-            params ^? hNodeLens . _QVarInstances . Lens.ix v <|>-            foralls ^? hNodeLens . _QVarInstances . Lens.ix v--{-# INLINE loadNominalDecl #-}-loadNominalDecl ::-    forall m typ.-    ( Monad m-    , HTraversable (NomVarTypes typ)-    , HNodesConstraint (NomVarTypes typ) (Unify m)-    , HasScheme (NomVarTypes typ) m typ-    ) =>-    Pure # NominalDecl typ ->-    m (LoadedNominalDecl typ # UVarOf m)-loadNominalDecl (Pure (NominalDecl params (Scheme foralls typ))) =-    do-        paramsL <- htraverse (Proxy @(Unify m) #> makeQVarInstances) params-        forallsL <- htraverse (Proxy @(Unify m) #> makeQVarInstances) foralls-        wrapM-            (Proxy @(HasScheme (NomVarTypes typ) m) #>>-                loadBody paramsL forallsL-            ) typ-            <&> LoadedNominalDecl paramsL forallsL--class MonadNominals nomId typ m where-    getNominalDecl :: nomId -> m (LoadedNominalDecl typ # UVarOf m)--class HasNominalInst nomId typ where-    nominalInst :: Prism' (typ # h) (NominalInst nomId (NomVarTypes typ) # h)--{-# INLINE lookupParams #-}-lookupParams ::-    forall m varTypes.-    ( Applicative m-    , HTraversable varTypes-    , HNodesConstraint varTypes (UnifyGen m)-    ) =>-    varTypes # QVarInstances (UVarOf m) ->-    m (varTypes # QVarInstances (UVarOf m))-lookupParams =-    htraverse (Proxy @(UnifyGen m) #> (_QVarInstances . traverse) lookupParam)-    where-        lookupParam :: forall t. UnifyGen m t => UVarOf m # t -> m (UVarOf m # t)-        lookupParam v =-            lookupVar binding v-            >>=-            \case-            UInstantiated r -> pure r-            USkolem l ->-                -- This is a phantom-type, wasn't instantiated by `instantiate`.-                scopeConstraints (Proxy @t) <&> (<> l) >>= newVar binding . UUnbound-            _ -> error "unexpected state at nominal's parameter"--type instance InferOf (ToNom n e) = NominalInst n (NomVarTypes (TypeOf e))--instance-    ( MonadScopeLevel m-    , MonadNominals nomId (TypeOf expr) m-    , HTraversable (NomVarTypes (TypeOf expr))-    , HNodesConstraint (NomVarTypes (TypeOf expr)) (UnifyGen m)-    , UnifyGen m (TypeOf expr)-    , HasInferredType expr-    , Infer m expr-    ) =>-    Infer m (ToNom nomId expr) where--    {-# INLINE inferBody #-}-    inferBody (ToNom nomId val) =-        do-            (InferredChild valI valR, typ, paramsT) <--                do-                    v <- inferChild val-                    LoadedNominalDecl params foralls gen <- getNominalDecl nomId-                    recover <--                        htraverse_-                        ( Proxy @(UnifyGen m) #>-                            traverse_ (instantiateForAll USkolem) . (^. _QVarInstances)-                        ) foralls-                        & execWriterT-                    (typ, paramsT) <- instantiateWith (lookupParams params) UUnbound gen-                    (v, typ, paramsT) <$ sequence_ recover-                & localLevel-            (ToNom nomId valI, NominalInst nomId paramsT)-                <$ unify typ (valR ^# inferredType (Proxy @expr))--type instance InferOf (FromNom _ e) = FuncType (TypeOf e)--instance-    ( Infer m expr-    , HasNominalInst nomId (TypeOf expr)-    , MonadNominals nomId (TypeOf expr) m-    , HTraversable (NomVarTypes (TypeOf expr))-    , HNodesConstraint (NomVarTypes (TypeOf expr)) (UnifyGen m)-    , UnifyGen m (TypeOf expr)-    ) =>-    Infer m (FromNom nomId expr) where--    {-# INLINE inferBody #-}-    inferBody (FromNom nomId) =-        do-            LoadedNominalDecl params _ gen <- getNominalDecl nomId-            (typ, paramsT) <- instantiateWith (lookupParams params) UUnbound gen-            nominalInst # NominalInst nomId paramsT & newTerm-                <&> (`FuncType` typ)-        <&> (FromNom nomId, )

@@ -1,163 +0,0 @@--- | Row types--{-# LANGUAGE FlexibleInstances, UndecidableInstances, FlexibleContexts, TemplateHaskell #-}--module Hyper.Type.AST.Row-    ( RowConstraints(..), RowKey-    , RowExtend(..), eKey, eVal, eRest, W_RowExtend(..)-    , FlatRowExtends(..), freExtends, freRest, W_FlatRowExtends(..)-    , MorphWitness(..)-    , flattenRow, flattenRowExtend, unflattenRow-    , verifyRowExtendConstraints, rowExtendStructureMismatch-    , rowElementInfer-    ) where--import           Control.Lens (Prism', Lens', contains)-import qualified Control.Lens as Lens-import           Control.Monad (foldM)-import qualified Data.Map as Map-import           Generics.Constraints (Constraints, makeDerivings, makeInstances)-import           Hyper-import           Hyper.Unify-import           Hyper.Unify.New (newTerm, newUnbound)-import           Hyper.Unify.Term (UTerm(..), _UTerm, UTermBody(..), uBody)-import           Text.Show.Combinators ((@|), showCon)--import           Hyper.Internal.Prelude--class-    (Ord (RowConstraintsKey constraints), TypeConstraints constraints) =>-    RowConstraints constraints where--    type RowConstraintsKey constraints-    forbidden :: Lens' constraints (Set (RowConstraintsKey constraints))--type RowKey typ = RowConstraintsKey (TypeConstraintsOf typ)---- | Row-extend primitive for use in both value-level and type-level-data RowExtend key val rest h = RowExtend-    { _eKey :: key-    , _eVal :: h :# val-    , _eRest :: h :# rest-    } deriving Generic--data FlatRowExtends key val rest h = FlatRowExtends-    { _freExtends :: Map key (h :# val)-    , _freRest :: h :# rest-    } deriving Generic--makeLenses ''RowExtend-makeLenses ''FlatRowExtends-makeCommonInstances [''FlatRowExtends]-makeZipMatch ''RowExtend-makeHContext ''RowExtend-makeHMorph ''RowExtend-makeHTraversableApplyAndBases ''RowExtend-makeHTraversableApplyAndBases ''FlatRowExtends-makeDerivings [''Eq, ''Ord] [''RowExtend]-makeInstances [''Binary, ''NFData] [''RowExtend]--instance-    Constraints (RowExtend key val rest h) Show =>-    Show (RowExtend key val rest h) where-    showsPrec p (RowExtend h v r) = (showCon "RowExtend" @| h @| v @| r) p--{-# INLINE flattenRowExtend #-}-flattenRowExtend ::-    (Ord key, Monad m) =>-    (v # rest -> m (Maybe (RowExtend key val rest # v))) ->-    RowExtend key val rest # v ->-    m (FlatRowExtends key val rest # v)-flattenRowExtend nextExtend (RowExtend h v rest) =-    flattenRow nextExtend rest-    <&> freExtends %~ Map.unionWith (error "Colliding keys") (Map.singleton h v)--{-# INLINE flattenRow #-}-flattenRow ::-    (Ord key, Monad m) =>-    (v # rest -> m (Maybe (RowExtend key val rest # v))) ->-    v # rest ->-    m (FlatRowExtends key val rest # v)-flattenRow nextExtend x =-    nextExtend x-    >>= maybe (pure (FlatRowExtends mempty x)) (flattenRowExtend nextExtend)--{-# INLINE unflattenRow #-}-unflattenRow ::-    Monad m =>-    (RowExtend key val rest # v -> m (v # rest)) ->-    FlatRowExtends key val rest # v -> m (v # rest)-unflattenRow mkExtend (FlatRowExtends fields rest) =-    fields ^@.. Lens.itraversed & foldM f rest-    where-        f acc (key, val) = RowExtend key val acc & mkExtend---- Helpers for Unify instances of type-level RowExtends:--{-# INLINE verifyRowExtendConstraints #-}-verifyRowExtendConstraints ::-    RowConstraints (TypeConstraintsOf rowTyp) =>-    (TypeConstraintsOf rowTyp -> TypeConstraintsOf valTyp) ->-    TypeConstraintsOf rowTyp ->-    RowExtend (RowKey rowTyp) valTyp rowTyp # h ->-    Maybe (RowExtend (RowKey rowTyp) valTyp rowTyp # WithConstraint h)-verifyRowExtendConstraints toChildC c (RowExtend h v rest)-    | c ^. forbidden . contains h = Nothing-    | otherwise =-        RowExtend h-        (WithConstraint (c & forbidden .~ mempty & toChildC) v)-        (WithConstraint (c & forbidden . contains h .~ True) rest)-        & Just--{-# INLINE rowExtendStructureMismatch #-}-rowExtendStructureMismatch ::-    Ord key =>-    ( Unify m rowTyp-    , Unify m valTyp-    ) =>-    (forall c. Unify m c => UVarOf m # c -> UVarOf m # c -> m (UVarOf m # c)) ->-    Prism' (rowTyp # UVarOf m) (RowExtend key valTyp rowTyp # UVarOf m) ->-    RowExtend key valTyp rowTyp # UVarOf m ->-    RowExtend key valTyp rowTyp # UVarOf m ->-    m ()-rowExtendStructureMismatch match extend r0 r1 =-    do-        flat0 <- flattenRowExtend nextExtend r0-        flat1 <- flattenRowExtend nextExtend r1-        Map.intersectionWith match (flat0 ^. freExtends) (flat1 ^. freExtends)-            & sequenceA_-        restVar <- UUnbound mempty & newVar binding-        let side x y =-                unflattenRow mkExtend FlatRowExtends-                { _freExtends =-                  (x ^. freExtends) `Map.difference` (y ^. freExtends)-                , _freRest = restVar-                } >>= match (y ^. freRest)-        _ <- side flat0 flat1-        _ <- side flat1 flat0-        pure ()-    where-        mkExtend ext = UTermBody mempty (extend # ext) & UTerm & newVar binding-        nextExtend v = semiPruneLookup v <&> (^? Lens._2 . _UTerm . uBody . extend)---- Helper for infering row usages of a row element,--- such as getting a field from a record or injecting into a sum type.--- Returns a unification variable for the element and for the whole row.-{-# INLINE rowElementInfer #-}-rowElementInfer ::-    forall m valTyp rowTyp.-    ( UnifyGen m valTyp-    , UnifyGen m rowTyp-    , RowConstraints (TypeConstraintsOf rowTyp)-    ) =>-    (RowExtend (RowKey rowTyp) valTyp rowTyp # UVarOf m -> rowTyp # UVarOf m) ->-    RowKey rowTyp ->-    m (UVarOf m # valTyp, UVarOf m # rowTyp)-rowElementInfer extendToRow h =-    do-        restVar <--            scopeConstraints (Proxy @rowTyp)-            >>= newVar binding . UUnbound . (forbidden . contains h .~ True)-        part <- newUnbound-        whole <- RowExtend h part restVar & extendToRow & newTerm-        pure (part, whole)