-- | Handles generating kind constraints to be fed to the kind
-- constraint solver (found in "Unison.KindInference.Solve").
module Unison.KindInference.Generate
  ( typeConstraints,
    termConstraints,
    declComponentConstraints,
    builtinConstraints,
  )
where

import Data.Foldable (foldlM)
import Data.Set qualified as Set
import U.Core.ABT qualified as ABT
import Unison.Builtin.Decls (rewriteTypeRef)
import Unison.Codebase.BuiltinAnnotation (BuiltinAnnotation (builtinAnnotation))
import Unison.ConstructorReference (GConstructorReference (..))
import Unison.DataDeclaration (Decl, asDataDecl)
import Unison.DataDeclaration qualified as DD
import Unison.Kind qualified as Unison
import Unison.KindInference.Constraint.Context (ConstraintContext (..))
import Unison.KindInference.Constraint.Provenance (Provenance (..))
import Unison.KindInference.Constraint.Provenance qualified as Provenance
import Unison.KindInference.Constraint.Unsolved (Constraint (..))
import Unison.KindInference.Generate.Monad (Gen, GeneratedConstraint, freshVar, lookupType, pushType, scopedType)
import Unison.KindInference.UVar (UVar)
import Unison.Prelude
import Unison.Reference (Reference)
import Unison.Term qualified as Term
import Unison.Type qualified as Type
import Unison.Util.Recursion
import Unison.Var (Type (User), Var (typed), freshIn)

--------------------------------------------------------------------------------
-- Constraints arising from Types
--------------------------------------------------------------------------------

-- | Generate kind constraints arising from a given type. The given
-- @UVar@ is constrained to have the kind of the given type.
typeConstraints :: (Var v, Ord loc) => UVar v loc -> Type.Type v loc -> Gen v loc [GeneratedConstraint v loc]
typeConstraints :: forall v loc.
(Var v, Ord loc) =>
UVar v loc -> Type v loc -> Gen v loc [GeneratedConstraint v loc]
typeConstraints UVar v loc
resultVar Type v loc
typ =
  TreeWalk -> ConstraintTree v loc -> [GeneratedConstraint v loc]
forall v loc.
TreeWalk -> ConstraintTree v loc -> [GeneratedConstraint v loc]
flatten TreeWalk
bottomUp (ConstraintTree v loc -> [GeneratedConstraint v loc])
-> Gen v loc (ConstraintTree v loc)
-> Gen v loc [GeneratedConstraint v loc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> UVar v loc -> Type v loc -> Gen v loc (ConstraintTree v loc)
forall v loc.
(Var v, Ord loc) =>
UVar v loc -> Type v loc -> Gen v loc (ConstraintTree v loc)
typeConstraintTree UVar v loc
resultVar Type v loc
typ

typeConstraintTree :: (Var v, Ord loc) => UVar v loc -> Type.Type v loc -> Gen v loc (ConstraintTree v loc)
typeConstraintTree :: forall v loc.
(Var v, Ord loc) =>
UVar v loc -> Type v loc -> Gen v loc (ConstraintTree v loc)
typeConstraintTree UVar v loc
resultVar term :: Type v loc
term@ABT.Term {loc
annotation :: loc
annotation :: forall (f :: * -> *) v a. Term f v a -> a
annotation, ABT F v (Type v loc)
out :: ABT F v (Type v loc)
out :: forall (f :: * -> *) v a. Term f v a -> ABT f v (Term f v a)
out} = do
  case ABT F v (Type v loc)
out of
    ABT.Abs v
_ Type v loc
_ -> [Char] -> Gen v loc (ConstraintTree v loc)
forall a. HasCallStack => [Char] -> a
error [Char]
"[typeConstraintTree] malformed type: Abs without an enclosing Forall or IntroOuter"
    ABT.Var v
v ->
      Type v loc -> Gen v loc (Maybe (UVar v loc))
forall v loc. Var v => Type v loc -> Gen v loc (Maybe (UVar v loc))
lookupType (loc -> v -> Type v loc
forall v a. Ord v => a -> v -> Type v a
Type.var loc
annotation v
v) Gen v loc (Maybe (UVar v loc))
-> (Maybe (UVar v loc) -> Gen v loc (ConstraintTree v loc))
-> Gen v loc (ConstraintTree v loc)
forall a b. Gen v loc a -> (a -> Gen v loc b) -> Gen v loc b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        Maybe (UVar v loc)
Nothing -> [Char] -> Gen v loc (ConstraintTree v loc)
forall a. HasCallStack => [Char] -> a
error ([Char]
"[typeConstraintTree] bug: encountered var " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> v -> [Char]
forall a. Show a => a -> [Char]
show v
v [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> [Char]
" missing from context")
        Just UVar v loc
x -> ConstraintTree v loc -> Gen v loc (ConstraintTree v loc)
forall a. a -> Gen v loc a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ConstraintTree v loc -> Gen v loc (ConstraintTree v loc))
-> ConstraintTree v loc -> Gen v loc (ConstraintTree v loc)
forall a b. (a -> b) -> a -> b
$ GeneratedConstraint v loc
-> ConstraintTree v loc -> ConstraintTree v loc
forall v loc.
GeneratedConstraint v loc
-> ConstraintTree v loc -> ConstraintTree v loc
Constraint (Provenance v loc
-> UVar v loc -> UVar v loc -> GeneratedConstraint v loc
forall uv v loc (typeProv :: * -> * -> *).
Provenance v loc -> uv -> uv -> Constraint uv v loc typeProv
Unify (ConstraintContext v loc -> loc -> Provenance v loc
forall v loc. ConstraintContext v loc -> loc -> Provenance v loc
Provenance ConstraintContext v loc
forall v loc. ConstraintContext v loc
ContextLookup loc
annotation) UVar v loc
resultVar UVar v loc
x) ([ConstraintTree v loc] -> ConstraintTree v loc
forall v loc. [ConstraintTree v loc] -> ConstraintTree v loc
Node [])
    ABT.Cycle Type v loc
_ -> [Char] -> Gen v loc (ConstraintTree v loc)
forall a. HasCallStack => [Char] -> a
error [Char]
"[typeConstraintTree] malformed type: Encountered Cycle in a type?"
    ABT.Tm F (Type v loc)
t0 -> case F (Type v loc)
t0 of
      Type.Arrow Type v loc
dom Type v loc
cod -> do
        let ctx :: ConstraintContext v loc
ctx = loc -> Type v loc -> Type v loc -> ConstraintContext v loc
forall v loc.
loc -> Type v loc -> Type v loc -> ConstraintContext v loc
AppArrow loc
annotation Type v loc
dom Type v loc
cod
        UVar v loc
k1 <- Type v loc -> Gen v loc (UVar v loc)
forall v loc. Var v => Type v loc -> Gen v loc (UVar v loc)
freshVar Type v loc
dom
        ConstraintTree v loc
domConstraints <- UVar v loc -> Type v loc -> Gen v loc (ConstraintTree v loc)
forall v loc.
(Var v, Ord loc) =>
UVar v loc -> Type v loc -> Gen v loc (ConstraintTree v loc)
typeConstraintTree UVar v loc
k1 Type v loc
dom
        UVar v loc
k2 <- Type v loc -> Gen v loc (UVar v loc)
forall v loc. Var v => Type v loc -> Gen v loc (UVar v loc)
freshVar Type v loc
cod
        ConstraintTree v loc
codConstraints <- UVar v loc -> Type v loc -> Gen v loc (ConstraintTree v loc)
forall v loc.
(Var v, Ord loc) =>
UVar v loc -> Type v loc -> Gen v loc (ConstraintTree v loc)
typeConstraintTree UVar v loc
k2 Type v loc
cod
        pure $
          GeneratedConstraint v loc
-> ConstraintTree v loc -> ConstraintTree v loc
forall v loc.
GeneratedConstraint v loc
-> ConstraintTree v loc -> ConstraintTree v loc
Constraint
            (UVar v loc -> Provenance v loc -> GeneratedConstraint v loc
forall uv v loc (typeProv :: * -> * -> *).
uv -> typeProv v loc -> Constraint uv v loc typeProv
IsType UVar v loc
resultVar (ConstraintContext v loc -> loc -> Provenance v loc
forall v loc. ConstraintContext v loc -> loc -> Provenance v loc
Provenance ConstraintContext v loc
ctx loc
annotation))
            ( [ConstraintTree v loc] -> ConstraintTree v loc
forall v loc. [ConstraintTree v loc] -> ConstraintTree v loc
Node
                [ GeneratedConstraint v loc
-> ConstraintTree v loc -> ConstraintTree v loc
forall v loc.
GeneratedConstraint v loc
-> ConstraintTree v loc -> ConstraintTree v loc
ParentConstraint (UVar v loc -> Provenance v loc -> GeneratedConstraint v loc
forall uv v loc (typeProv :: * -> * -> *).
uv -> typeProv v loc -> Constraint uv v loc typeProv
IsType UVar v loc
k1 (ConstraintContext v loc -> loc -> Provenance v loc
forall v loc. ConstraintContext v loc -> loc -> Provenance v loc
Provenance ConstraintContext v loc
ctx (loc -> Provenance v loc) -> loc -> Provenance v loc
forall a b. (a -> b) -> a -> b
$ Type v loc -> loc
forall (f :: * -> *) v a. Term f v a -> a
ABT.annotation Type v loc
dom)) ConstraintTree v loc
domConstraints,
                  GeneratedConstraint v loc
-> ConstraintTree v loc -> ConstraintTree v loc
forall v loc.
GeneratedConstraint v loc
-> ConstraintTree v loc -> ConstraintTree v loc
ParentConstraint (UVar v loc -> Provenance v loc -> GeneratedConstraint v loc
forall uv v loc (typeProv :: * -> * -> *).
uv -> typeProv v loc -> Constraint uv v loc typeProv
IsType UVar v loc
k2 (ConstraintContext v loc -> loc -> Provenance v loc
forall v loc. ConstraintContext v loc -> loc -> Provenance v loc
Provenance ConstraintContext v loc
ctx (loc -> Provenance v loc) -> loc -> Provenance v loc
forall a b. (a -> b) -> a -> b
$ Type v loc -> loc
forall (f :: * -> *) v a. Term f v a -> a
ABT.annotation Type v loc
cod)) ConstraintTree v loc
codConstraints
                ]
            )
      Type.App Type v loc
abs Type v loc
arg -> do
        UVar v loc
absVar <- Type v loc -> Gen v loc (UVar v loc)
forall v loc. Var v => Type v loc -> Gen v loc (UVar v loc)
freshVar Type v loc
abs
        UVar v loc
absArgVar <- Type v loc -> Gen v loc (UVar v loc)
forall v loc. Var v => Type v loc -> Gen v loc (UVar v loc)
freshVar Type v loc
arg
        ConstraintTree v loc
absConstraints <- UVar v loc -> Type v loc -> Gen v loc (ConstraintTree v loc)
forall v loc.
(Var v, Ord loc) =>
UVar v loc -> Type v loc -> Gen v loc (ConstraintTree v loc)
typeConstraintTree UVar v loc
absVar Type v loc
abs
        UVar v loc
argVar <- Type v loc -> Gen v loc (UVar v loc)
forall v loc. Var v => Type v loc -> Gen v loc (UVar v loc)
freshVar Type v loc
arg
        ConstraintTree v loc
argConstraints <- UVar v loc -> Type v loc -> Gen v loc (ConstraintTree v loc)
forall v loc.
(Var v, Ord loc) =>
UVar v loc -> Type v loc -> Gen v loc (ConstraintTree v loc)
typeConstraintTree UVar v loc
argVar Type v loc
arg
        let wellKindedAbs :: GeneratedConstraint v loc
wellKindedAbs = UVar v loc
-> Provenance v loc
-> UVar v loc
-> UVar v loc
-> GeneratedConstraint v loc
forall uv v loc (typeProv :: * -> * -> *).
uv -> Provenance v loc -> uv -> uv -> Constraint uv v loc typeProv
IsArr UVar v loc
absVar (ConstraintContext v loc -> loc -> Provenance v loc
forall v loc. ConstraintContext v loc -> loc -> Provenance v loc
Provenance (UVar v loc -> UVar v loc -> ConstraintContext v loc
forall v loc. UVar v loc -> UVar v loc -> ConstraintContext v loc
AppAbs UVar v loc
absVar UVar v loc
absArgVar) (Type v loc -> loc
forall (f :: * -> *) v a. Term f v a -> a
ABT.annotation Type v loc
abs)) UVar v loc
absArgVar UVar v loc
resultVar
            applicationUnification :: GeneratedConstraint v loc
applicationUnification = Provenance v loc
-> UVar v loc -> UVar v loc -> GeneratedConstraint v loc
forall uv v loc (typeProv :: * -> * -> *).
Provenance v loc -> uv -> uv -> Constraint uv v loc typeProv
Unify (ConstraintContext v loc -> loc -> Provenance v loc
forall v loc. ConstraintContext v loc -> loc -> Provenance v loc
Provenance (UVar v loc -> UVar v loc -> UVar v loc -> ConstraintContext v loc
forall v loc.
UVar v loc -> UVar v loc -> UVar v loc -> ConstraintContext v loc
AppArg UVar v loc
absVar UVar v loc
absArgVar UVar v loc
argVar) (Type v loc -> loc
forall (f :: * -> *) v a. Term f v a -> a
ABT.annotation Type v loc
arg)) UVar v loc
absArgVar UVar v loc
argVar
        pure $
          GeneratedConstraint v loc
-> ConstraintTree v loc -> ConstraintTree v loc
forall v loc.
GeneratedConstraint v loc
-> ConstraintTree v loc -> ConstraintTree v loc
Constraint
            GeneratedConstraint v loc
applicationUnification
            ( [ConstraintTree v loc] -> ConstraintTree v loc
forall v loc. [ConstraintTree v loc] -> ConstraintTree v loc
Node
                [ GeneratedConstraint v loc
-> ConstraintTree v loc -> ConstraintTree v loc
forall v loc.
GeneratedConstraint v loc
-> ConstraintTree v loc -> ConstraintTree v loc
ParentConstraint GeneratedConstraint v loc
wellKindedAbs ConstraintTree v loc
absConstraints,
                  ConstraintTree v loc
argConstraints
                ]
            )
      Type.Forall ABT.Term {loc
annotation :: forall (f :: * -> *) v a. Term f v a -> a
annotation :: loc
annotation, ABT F v (Type v loc)
out :: forall (f :: * -> *) v a. Term f v a -> ABT f v (Term f v a)
out :: ABT F v (Type v loc)
out} -> case ABT F v (Type v loc)
out of
        ABT.Abs v
v Type v loc
x ->
          Type v loc
-> (UVar v loc -> Gen v loc (ConstraintTree v loc))
-> Gen v loc (ConstraintTree v loc)
forall v loc r.
Var v =>
Type v loc -> (UVar v loc -> Gen v loc r) -> Gen v loc r
scopedType (loc -> v -> Type v loc
forall v a. Ord v => a -> v -> Type v a
Type.var loc
annotation v
v) \UVar v loc
_ -> do
            UVar v loc -> Type v loc -> Gen v loc (ConstraintTree v loc)
forall v loc.
(Var v, Ord loc) =>
UVar v loc -> Type v loc -> Gen v loc (ConstraintTree v loc)
typeConstraintTree UVar v loc
resultVar Type v loc
x
        ABT F v (Type v loc)
_ -> [Char] -> Gen v loc (ConstraintTree v loc)
forall a. HasCallStack => [Char] -> a
error [Char]
"[typeConstraintTree] Forall wrapping a non-abs"
      Type.IntroOuter ABT.Term {loc
annotation :: forall (f :: * -> *) v a. Term f v a -> a
annotation :: loc
annotation, ABT F v (Type v loc)
out :: forall (f :: * -> *) v a. Term f v a -> ABT f v (Term f v a)
out :: ABT F v (Type v loc)
out} -> case ABT F v (Type v loc)
out of
        ABT.Abs v
v Type v loc
x -> v
-> loc
-> (GeneratedConstraint v loc -> Gen v loc (ConstraintTree v loc))
-> Gen v loc (ConstraintTree v loc)
forall v loc r.
Var v =>
v
-> loc -> (GeneratedConstraint v loc -> Gen v loc r) -> Gen v loc r
handleIntroOuter v
v loc
annotation (\GeneratedConstraint v loc
c -> GeneratedConstraint v loc
-> ConstraintTree v loc -> ConstraintTree v loc
forall v loc.
GeneratedConstraint v loc
-> ConstraintTree v loc -> ConstraintTree v loc
Constraint GeneratedConstraint v loc
c (ConstraintTree v loc -> ConstraintTree v loc)
-> Gen v loc (ConstraintTree v loc)
-> Gen v loc (ConstraintTree v loc)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> UVar v loc -> Type v loc -> Gen v loc (ConstraintTree v loc)
forall v loc.
(Var v, Ord loc) =>
UVar v loc -> Type v loc -> Gen v loc (ConstraintTree v loc)
typeConstraintTree UVar v loc
resultVar Type v loc
x)
        ABT F v (Type v loc)
_ -> [Char] -> Gen v loc (ConstraintTree v loc)
forall a. HasCallStack => [Char] -> a
error [Char]
"[typeConstraintTree] IntroOuter wrapping a non-abs"
      Type.Ann Type v loc
x Kind
kind -> do
        ConstraintTree v loc
ct <- UVar v loc -> Type v loc -> Gen v loc (ConstraintTree v loc)
forall v loc.
(Var v, Ord loc) =>
UVar v loc -> Type v loc -> Gen v loc (ConstraintTree v loc)
typeConstraintTree UVar v loc
resultVar Type v loc
x
        [GeneratedConstraint v loc]
gcs <- Provenance v loc
-> UVar v loc -> Kind -> Gen v loc [GeneratedConstraint v loc]
forall v loc.
Var v =>
Provenance v loc
-> UVar v loc -> Kind -> Gen v loc [GeneratedConstraint v loc]
constrainToKind (ConstraintContext v loc -> loc -> Provenance v loc
forall v loc. ConstraintContext v loc -> loc -> Provenance v loc
Provenance ConstraintContext v loc
forall v loc. ConstraintContext v loc
Annotation loc
annotation) UVar v loc
resultVar (Kind -> Kind
fromUnisonKind Kind
kind)
        pure ((GeneratedConstraint v loc
 -> ConstraintTree v loc -> ConstraintTree v loc)
-> ConstraintTree v loc
-> [GeneratedConstraint v loc]
-> ConstraintTree v loc
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr GeneratedConstraint v loc
-> ConstraintTree v loc -> ConstraintTree v loc
forall v loc.
GeneratedConstraint v loc
-> ConstraintTree v loc -> ConstraintTree v loc
Constraint ConstraintTree v loc
ct [GeneratedConstraint v loc]
gcs)
      Type.Ref TypeReference
r ->
        Type v loc -> Gen v loc (Maybe (UVar v loc))
forall v loc. Var v => Type v loc -> Gen v loc (Maybe (UVar v loc))
lookupType (loc -> TypeReference -> Type v loc
forall v a. Ord v => a -> TypeReference -> Type v a
Type.ref loc
annotation TypeReference
r) Gen v loc (Maybe (UVar v loc))
-> (Maybe (UVar v loc) -> Gen v loc (ConstraintTree v loc))
-> Gen v loc (ConstraintTree v loc)
forall a b. Gen v loc a -> (a -> Gen v loc b) -> Gen v loc b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
          Maybe (UVar v loc)
Nothing -> [Char] -> Gen v loc (ConstraintTree v loc)
forall a. HasCallStack => [Char] -> a
error ([Char]
"[typeConstraintTree] Ref lookup failure: " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> Type v loc -> [Char]
forall a. Show a => a -> [Char]
show Type v loc
term)
          Just UVar v loc
x -> ConstraintTree v loc -> Gen v loc (ConstraintTree v loc)
forall a. a -> Gen v loc a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ConstraintTree v loc -> Gen v loc (ConstraintTree v loc))
-> ConstraintTree v loc -> Gen v loc (ConstraintTree v loc)
forall a b. (a -> b) -> a -> b
$ GeneratedConstraint v loc
-> ConstraintTree v loc -> ConstraintTree v loc
forall v loc.
GeneratedConstraint v loc
-> ConstraintTree v loc -> ConstraintTree v loc
Constraint (Provenance v loc
-> UVar v loc -> UVar v loc -> GeneratedConstraint v loc
forall uv v loc (typeProv :: * -> * -> *).
Provenance v loc -> uv -> uv -> Constraint uv v loc typeProv
Unify (ConstraintContext v loc -> loc -> Provenance v loc
forall v loc. ConstraintContext v loc -> loc -> Provenance v loc
Provenance ConstraintContext v loc
forall v loc. ConstraintContext v loc
ContextLookup loc
annotation) UVar v loc
resultVar UVar v loc
x) ([ConstraintTree v loc] -> ConstraintTree v loc
forall v loc. [ConstraintTree v loc] -> ConstraintTree v loc
Node [])
      Type.Effect Type v loc
effTyp Type v loc
b -> do
        UVar v loc
effKind <- Type v loc -> Gen v loc (UVar v loc)
forall v loc. Var v => Type v loc -> Gen v loc (UVar v loc)
freshVar Type v loc
effTyp
        ConstraintTree v loc
effConstraints <- UVar v loc -> Type v loc -> Gen v loc (ConstraintTree v loc)
forall v loc.
(Var v, Ord loc) =>
UVar v loc -> Type v loc -> Gen v loc (ConstraintTree v loc)
typeConstraintTree UVar v loc
effKind Type v loc
effTyp
        ConstraintTree v loc
restConstraints <- UVar v loc -> Type v loc -> Gen v loc (ConstraintTree v loc)
forall v loc.
(Var v, Ord loc) =>
UVar v loc -> Type v loc -> Gen v loc (ConstraintTree v loc)
typeConstraintTree UVar v loc
resultVar Type v loc
b
        pure $ [ConstraintTree v loc] -> ConstraintTree v loc
forall v loc. [ConstraintTree v loc] -> ConstraintTree v loc
Node [ConstraintTree v loc
effConstraints, ConstraintTree v loc
restConstraints]
      Type.Effects [Type v loc]
effs -> do
        GeneratedConstraint v loc
-> ConstraintTree v loc -> ConstraintTree v loc
forall v loc.
GeneratedConstraint v loc
-> ConstraintTree v loc -> ConstraintTree v loc
ParentConstraint (UVar v loc -> Provenance v loc -> GeneratedConstraint v loc
forall uv v loc (typeProv :: * -> * -> *).
uv -> Provenance v loc -> Constraint uv v loc typeProv
IsAbility UVar v loc
resultVar (ConstraintContext v loc -> loc -> Provenance v loc
forall v loc. ConstraintContext v loc -> loc -> Provenance v loc
Provenance ConstraintContext v loc
forall v loc. ConstraintContext v loc
EffectsList loc
annotation)) (ConstraintTree v loc -> ConstraintTree v loc)
-> ([ConstraintTree v loc] -> ConstraintTree v loc)
-> [ConstraintTree v loc]
-> ConstraintTree v loc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [ConstraintTree v loc] -> ConstraintTree v loc
forall v loc. [ConstraintTree v loc] -> ConstraintTree v loc
Node ([ConstraintTree v loc] -> ConstraintTree v loc)
-> Gen v loc [ConstraintTree v loc]
-> Gen v loc (ConstraintTree v loc)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Type v loc]
-> (Type v loc -> Gen v loc (ConstraintTree v loc))
-> Gen v loc [ConstraintTree v loc]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for [Type v loc]
effs \Type v loc
eff -> do
          UVar v loc
effKind <- Type v loc -> Gen v loc (UVar v loc)
forall v loc. Var v => Type v loc -> Gen v loc (UVar v loc)
freshVar Type v loc
eff
          ConstraintTree v loc
effConstraints <- UVar v loc -> Type v loc -> Gen v loc (ConstraintTree v loc)
forall v loc.
(Var v, Ord loc) =>
UVar v loc -> Type v loc -> Gen v loc (ConstraintTree v loc)
typeConstraintTree UVar v loc
effKind Type v loc
eff
          pure $ GeneratedConstraint v loc
-> ConstraintTree v loc -> ConstraintTree v loc
forall v loc.
GeneratedConstraint v loc
-> ConstraintTree v loc -> ConstraintTree v loc
ParentConstraint (UVar v loc -> Provenance v loc -> GeneratedConstraint v loc
forall uv v loc (typeProv :: * -> * -> *).
uv -> Provenance v loc -> Constraint uv v loc typeProv
IsAbility UVar v loc
effKind (ConstraintContext v loc -> loc -> Provenance v loc
forall v loc. ConstraintContext v loc -> loc -> Provenance v loc
Provenance ConstraintContext v loc
forall v loc. ConstraintContext v loc
EffectsList (loc -> Provenance v loc) -> loc -> Provenance v loc
forall a b. (a -> b) -> a -> b
$ Type v loc -> loc
forall (f :: * -> *) v a. Term f v a -> a
ABT.annotation Type v loc
eff)) ConstraintTree v loc
effConstraints

handleIntroOuter :: (Var v) => v -> loc -> (GeneratedConstraint v loc -> Gen v loc r) -> Gen v loc r
handleIntroOuter :: forall v loc r.
Var v =>
v
-> loc -> (GeneratedConstraint v loc -> Gen v loc r) -> Gen v loc r
handleIntroOuter v
v loc
loc GeneratedConstraint v loc -> Gen v loc r
k = do
  let typ :: Type v loc
typ = loc -> v -> Type v loc
forall v a. Ord v => a -> v -> Type v a
Type.var loc
loc v
v
  UVar v loc
new <- Type v loc -> Gen v loc (UVar v loc)
forall v loc. Var v => Type v loc -> Gen v loc (UVar v loc)
freshVar Type v loc
typ
  UVar v loc
orig <-
    Type v loc -> Gen v loc (Maybe (UVar v loc))
forall v loc. Var v => Type v loc -> Gen v loc (Maybe (UVar v loc))
lookupType Type v loc
typ Gen v loc (Maybe (UVar v loc))
-> (Maybe (UVar v loc) -> Gen v loc (UVar v loc))
-> Gen v loc (UVar v loc)
forall a b. Gen v loc a -> (a -> Gen v loc b) -> Gen v loc b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      Maybe (UVar v loc)
Nothing -> [Char] -> Gen v loc (UVar v loc)
forall a. HasCallStack => [Char] -> a
error [Char]
"[malformed type] IntroOuter not in lexical scope of matching Forall"
      Just UVar v loc
a -> UVar v loc -> Gen v loc (UVar v loc)
forall a. a -> Gen v loc a
forall (f :: * -> *) a. Applicative f => a -> f a
pure UVar v loc
a
  GeneratedConstraint v loc -> Gen v loc r
k (Provenance v loc
-> UVar v loc -> UVar v loc -> GeneratedConstraint v loc
forall uv v loc (typeProv :: * -> * -> *).
Provenance v loc -> uv -> uv -> Constraint uv v loc typeProv
Unify (ConstraintContext v loc -> loc -> Provenance v loc
forall v loc. ConstraintContext v loc -> loc -> Provenance v loc
Provenance ConstraintContext v loc
forall v loc. ConstraintContext v loc
ScopeReference loc
loc) UVar v loc
new UVar v loc
orig)

--------------------------------------------------------------------------------
-- Constraints arising from Type annotations
--------------------------------------------------------------------------------

-- | Check that all annotations in a term are well-kinded
termConstraints :: forall v loc. (Var v, Ord loc) => Term.Term v loc -> Gen v loc [GeneratedConstraint v loc]
termConstraints :: forall v loc.
(Var v, Ord loc) =>
Term v loc -> Gen v loc [GeneratedConstraint v loc]
termConstraints Term v loc
x = TreeWalk -> ConstraintTree v loc -> [GeneratedConstraint v loc]
forall v loc.
TreeWalk -> ConstraintTree v loc -> [GeneratedConstraint v loc]
flatten TreeWalk
bottomUp (ConstraintTree v loc -> [GeneratedConstraint v loc])
-> Gen v loc (ConstraintTree v loc)
-> Gen v loc [GeneratedConstraint v loc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term v loc -> Gen v loc (ConstraintTree v loc)
forall v loc.
(Var v, Ord loc) =>
Term v loc -> Gen v loc (ConstraintTree v loc)
termConstraintTree Term v loc
x

termConstraintTree :: forall v loc. (Var v, Ord loc) => Term.Term v loc -> Gen v loc (ConstraintTree v loc)
termConstraintTree :: forall v loc.
(Var v, Ord loc) =>
Term v loc -> Gen v loc (ConstraintTree v loc)
termConstraintTree = ([ConstraintTree v loc] -> ConstraintTree v loc)
-> Gen v loc [ConstraintTree v loc]
-> Gen v loc (ConstraintTree v loc)
forall a b. (a -> b) -> Gen v loc a -> Gen v loc b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [ConstraintTree v loc] -> ConstraintTree v loc
forall v loc. [ConstraintTree v loc] -> ConstraintTree v loc
Node (Gen v loc [ConstraintTree v loc]
 -> Gen v loc (ConstraintTree v loc))
-> (Term v loc -> Gen v loc [ConstraintTree v loc])
-> Term v loc
-> Gen v loc (ConstraintTree v loc)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (loc
 -> Type v loc
 -> Gen v loc [ConstraintTree v loc]
 -> Gen v loc [ConstraintTree v loc])
-> (Gen v loc [ConstraintTree v loc]
    -> Gen v loc [ConstraintTree v loc]
    -> Gen v loc [ConstraintTree v loc])
-> Gen v loc [ConstraintTree v loc]
-> Term v loc
-> Gen v loc [ConstraintTree v loc]
forall loc v b.
(loc -> Type v loc -> b -> b)
-> (b -> b -> b) -> b -> Term v loc -> b
dfAnns loc
-> Type v loc
-> Gen v loc [ConstraintTree v loc]
-> Gen v loc [ConstraintTree v loc]
processAnn Gen v loc [ConstraintTree v loc]
-> Gen v loc [ConstraintTree v loc]
-> Gen v loc [ConstraintTree v loc]
forall {f :: * -> *} {a}. Applicative f => f [a] -> f [a] -> f [a]
cons Gen v loc [ConstraintTree v loc]
forall {a}. Gen v loc [a]
nil (Term v loc -> Gen v loc [ConstraintTree v loc])
-> (Term v loc -> Term v loc)
-> Term v loc
-> Gen v loc [ConstraintTree v loc]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term v loc -> Term v loc
forall v loc. Ord v => Term v loc -> Term v loc
hackyStripAnns
  where
    processAnn :: loc -> Type.Type v loc -> Gen v loc [ConstraintTree v loc] -> Gen v loc [ConstraintTree v loc]
    processAnn :: loc
-> Type v loc
-> Gen v loc [ConstraintTree v loc]
-> Gen v loc [ConstraintTree v loc]
processAnn loc
ann Type v loc
typ Gen v loc [ConstraintTree v loc]
mrest = do
      Type v loc
-> (Type v loc
    -> [GeneratedConstraint v loc] -> Gen v loc [ConstraintTree v loc])
-> Gen v loc [ConstraintTree v loc]
forall v loc r.
(Var v, Ord loc) =>
Type v loc
-> (Type v loc -> [GeneratedConstraint v loc] -> Gen v loc r)
-> Gen v loc r
instantiateType Type v loc
typ \Type v loc
typ [GeneratedConstraint v loc]
gcs -> do
        UVar v loc
typKind <- Type v loc -> Gen v loc (UVar v loc)
forall v loc. Var v => Type v loc -> Gen v loc (UVar v loc)
freshVar Type v loc
typ
        ConstraintTree v loc
annConstraints <- GeneratedConstraint v loc
-> ConstraintTree v loc -> ConstraintTree v loc
forall v loc.
GeneratedConstraint v loc
-> ConstraintTree v loc -> ConstraintTree v loc
ParentConstraint (UVar v loc -> Provenance v loc -> GeneratedConstraint v loc
forall uv v loc (typeProv :: * -> * -> *).
uv -> typeProv v loc -> Constraint uv v loc typeProv
IsType UVar v loc
typKind (ConstraintContext v loc -> loc -> Provenance v loc
forall v loc. ConstraintContext v loc -> loc -> Provenance v loc
Provenance ConstraintContext v loc
forall v loc. ConstraintContext v loc
TypeAnnotation loc
ann)) (ConstraintTree v loc -> ConstraintTree v loc)
-> Gen v loc (ConstraintTree v loc)
-> Gen v loc (ConstraintTree v loc)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> UVar v loc -> Type v loc -> Gen v loc (ConstraintTree v loc)
forall v loc.
(Var v, Ord loc) =>
UVar v loc -> Type v loc -> Gen v loc (ConstraintTree v loc)
typeConstraintTree UVar v loc
typKind Type v loc
typ
        let annConstraints' :: ConstraintTree v loc
annConstraints' = (GeneratedConstraint v loc
 -> ConstraintTree v loc -> ConstraintTree v loc)
-> ConstraintTree v loc
-> [GeneratedConstraint v loc]
-> ConstraintTree v loc
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr GeneratedConstraint v loc
-> ConstraintTree v loc -> ConstraintTree v loc
forall v loc.
GeneratedConstraint v loc
-> ConstraintTree v loc -> ConstraintTree v loc
Constraint ConstraintTree v loc
annConstraints [GeneratedConstraint v loc]
gcs
        [ConstraintTree v loc]
rest <- Gen v loc [ConstraintTree v loc]
mrest
        pure (ConstraintTree v loc
annConstraints' ConstraintTree v loc
-> [ConstraintTree v loc] -> [ConstraintTree v loc]
forall a. a -> [a] -> [a]
: [ConstraintTree v loc]
rest)
    cons :: f [a] -> f [a] -> f [a]
cons f [a]
mlhs f [a]
mrhs = [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
(++) ([a] -> [a] -> [a]) -> f [a] -> f ([a] -> [a])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f [a]
mlhs f ([a] -> [a]) -> f [a] -> f [a]
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> f [a]
mrhs
    nil :: Gen v loc [a]
nil = [a] -> Gen v loc [a]
forall a. a -> Gen v loc a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []

-- | Helper for @termConstraints@ that instantiates the outermost
-- foralls and keeps the type in scope (in the type map) while
-- checking lexically nested type annotations.
instantiateType ::
  forall v loc r.
  (Var v, Ord loc) =>
  Type.Type v loc ->
  (Type.Type v loc -> [GeneratedConstraint v loc] -> Gen v loc r) ->
  Gen v loc r
instantiateType :: forall v loc r.
(Var v, Ord loc) =>
Type v loc
-> (Type v loc -> [GeneratedConstraint v loc] -> Gen v loc r)
-> Gen v loc r
instantiateType Type v loc
type0 Type v loc -> [GeneratedConstraint v loc] -> Gen v loc r
k =
  let go :: [GeneratedConstraint v loc] -> Type v loc -> Gen v loc r
go [GeneratedConstraint v loc]
acc = \case
        ABT.Tm' (Type.Forall ABT.Term {loc
annotation :: forall (f :: * -> *) v a. Term f v a -> a
annotation :: loc
annotation, out :: forall (f :: * -> *) v a. Term f v a -> ABT f v (Term f v a)
out = ABT.Abs v
x Type v loc
t}) -> do
          Type v loc -> (UVar v loc -> Gen v loc r) -> Gen v loc r
forall v loc r.
Var v =>
Type v loc -> (UVar v loc -> Gen v loc r) -> Gen v loc r
scopedType (loc -> v -> Type v loc
forall v a. Ord v => a -> v -> Type v a
Type.var loc
annotation v
x) \UVar v loc
_ -> do
            [GeneratedConstraint v loc] -> Type v loc -> Gen v loc r
go [GeneratedConstraint v loc]
acc Type v loc
t
        ABT.Tm' (Type.IntroOuter ABT.Term {loc
annotation :: forall (f :: * -> *) v a. Term f v a -> a
annotation :: loc
annotation, out :: forall (f :: * -> *) v a. Term f v a -> ABT f v (Term f v a)
out = ABT.Abs v
x Type v loc
t}) -> do
          v
-> loc -> (GeneratedConstraint v loc -> Gen v loc r) -> Gen v loc r
forall v loc r.
Var v =>
v
-> loc -> (GeneratedConstraint v loc -> Gen v loc r) -> Gen v loc r
handleIntroOuter v
x loc
annotation \GeneratedConstraint v loc
c -> [GeneratedConstraint v loc] -> Type v loc -> Gen v loc r
go (GeneratedConstraint v loc
c GeneratedConstraint v loc
-> [GeneratedConstraint v loc] -> [GeneratedConstraint v loc]
forall a. a -> [a] -> [a]
: [GeneratedConstraint v loc]
acc) Type v loc
t
        Type v loc
t -> Type v loc -> [GeneratedConstraint v loc] -> Gen v loc r
k Type v loc
t ([GeneratedConstraint v loc] -> [GeneratedConstraint v loc]
forall a. [a] -> [a]
reverse [GeneratedConstraint v loc]
acc)
   in [GeneratedConstraint v loc] -> Type v loc -> Gen v loc r
go [] Type v loc
type0

-- | Process type annotations depth-first. Allows processing
-- annotations with lexical scoping.
dfAnns :: (loc -> Type.Type v loc -> b -> b) -> (b -> b -> b) -> b -> Term.Term v loc -> b
dfAnns :: forall loc v b.
(loc -> Type v loc -> b -> b)
-> (b -> b -> b) -> b -> Term v loc -> b
dfAnns loc -> Type v loc -> b -> b
annAlg b -> b -> b
cons b
nil = Algebra (Term' (F v loc loc) v loc) b -> Term v loc -> b
forall a. Algebra (Term' (F v loc loc) v loc) a -> Term v loc -> a
forall t (f :: * -> *) a. Recursive t f => Algebra f a -> t -> a
cata \(ABT.Term' Set v
_ loc
ann ABT (F v loc loc) v b
abt0) -> case ABT (F v loc loc) v b
abt0 of
  ABT.Var v
_ -> b
nil
  ABT.Cycle b
x -> b
x
  ABT.Abs v
_ b
x -> b
x
  ABT.Tm F v loc loc b
t -> case F v loc loc b
t of
    Term.Ann b
trm Type v loc
typ -> loc -> Type v loc -> b -> b
annAlg loc
ann Type v loc
typ b
trm
    F v loc loc b
x -> (b -> b -> b) -> b -> F v loc loc b -> b
forall a b. (a -> b -> b) -> b -> F v loc loc a -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr b -> b -> b
cons b
nil F v loc loc b
x

-- Our rewrite signature machinery generates type annotations that are
-- not well kinded. Work around this for now by stripping those
-- annotations.
hackyStripAnns :: (Ord v) => Term.Term v loc -> Term.Term v loc
hackyStripAnns :: forall v loc. Ord v => Term v loc -> Term v loc
hackyStripAnns =
  (Bool, Term v loc) -> Term v loc
forall a b. (a, b) -> b
snd ((Bool, Term v loc) -> Term v loc)
-> (Term v loc -> (Bool, Term v loc)) -> Term v loc -> Term v loc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Algebra (Term' (F v loc loc) v loc) (Bool, Term v loc)
-> Term v loc -> (Bool, Term v loc)
forall a. Algebra (Term' (F v loc loc) v loc) a -> Term v loc -> a
forall t (f :: * -> *) a. Recursive t f => Algebra f a -> t -> a
cata \(ABT.Term' Set v
_ loc
ann ABT (F v loc loc) v (Bool, Term v loc)
abt0) -> case ABT (F v loc loc) v (Bool, Term v loc)
abt0 of
    ABT.Var v
v -> (Bool
False, loc -> v -> Term v loc
forall a v (f :: * -> *). a -> v -> Term f v a
ABT.var loc
ann v
v)
    ABT.Cycle (Bool
_, Term v loc
x) -> (Bool
False, loc -> Term v loc -> Term v loc
forall a (f :: * -> *) v. a -> Term f v a -> Term f v a
ABT.cycle loc
ann Term v loc
x)
    ABT.Abs v
v (Bool
_, Term v loc
x) -> (Bool
False, loc -> v -> Term v loc -> Term v loc
forall v a (f :: * -> *).
Ord v =>
a -> v -> Term f v a -> Term f v a
ABT.abs loc
ann v
v Term v loc
x)
    ABT.Tm F v loc loc (Bool, Term v loc)
tm0 -> case F v loc loc (Bool, Term v loc)
tm0 of
      Term.App (Bool
isHack, Term v loc
abs) (Bool
_, Term v loc
arg) ->
        let argMod :: Term v loc -> Term v loc
argMod = case Bool
isHack of
              Bool
True -> Term v loc -> Term v loc
stripAnns
              Bool
False -> Term v loc -> Term v loc
forall a. a -> a
id
         in (Bool
isHack, loc -> Term v loc -> Term v loc -> Term v loc
forall v a vt at ap.
Ord v =>
a -> Term2 vt at ap v a -> Term2 vt at ap v a -> Term2 vt at ap v a
Term.app loc
ann Term v loc
abs (Term v loc -> Term v loc
argMod Term v loc
arg))
      Term.Constructor cref :: ConstructorReference
cref@(ConstructorReference TypeReference
r ConstructorId
_) ->
        let isHack :: Bool
isHack = TypeReference
r TypeReference -> TypeReference -> Bool
forall a. Eq a => a -> a -> Bool
== TypeReference
rewriteTypeRef
         in (Bool
isHack, loc -> ConstructorReference -> Term v loc
forall v a vt at ap.
Ord v =>
a -> ConstructorReference -> Term2 vt at ap v a
Term.constructor loc
ann ConstructorReference
cref)
      F v loc loc (Bool, Term v loc)
t -> (Bool
False, loc -> F v loc loc (Term v loc) -> Term v loc
forall (f :: * -> *) v a.
(Foldable f, Ord v) =>
a -> f (Term f v a) -> Term f v a
ABT.tm loc
ann ((Bool, Term v loc) -> Term v loc
forall a b. (a, b) -> b
snd ((Bool, Term v loc) -> Term v loc)
-> F v loc loc (Bool, Term v loc) -> F v loc loc (Term v loc)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> F v loc loc (Bool, Term v loc)
t))
  where
    stripAnns :: Term v loc -> Term v loc
stripAnns = Algebra (Term' (F v loc loc) v loc) (Term v loc)
-> Term v loc -> Term v loc
forall a. Algebra (Term' (F v loc loc) v loc) a -> Term v loc -> a
forall t (f :: * -> *) a. Recursive t f => Algebra f a -> t -> a
cata \(ABT.Term' Set v
_ loc
ann ABT (F v loc loc) v (Term v loc)
abt0) -> case ABT (F v loc loc) v (Term v loc)
abt0 of
      ABT.Var v
v -> loc -> v -> Term v loc
forall a v (f :: * -> *). a -> v -> Term f v a
ABT.var loc
ann v
v
      ABT.Cycle Term v loc
x -> loc -> Term v loc -> Term v loc
forall a (f :: * -> *) v. a -> Term f v a -> Term f v a
ABT.cycle loc
ann Term v loc
x
      ABT.Abs v
v Term v loc
x -> loc -> v -> Term v loc -> Term v loc
forall v a (f :: * -> *).
Ord v =>
a -> v -> Term f v a -> Term f v a
ABT.abs loc
ann v
v Term v loc
x
      ABT.Tm F v loc loc (Term v loc)
tm0 -> case F v loc loc (Term v loc)
tm0 of
        Term.Ann Term v loc
trm Type v loc
_typ -> Term v loc
trm
        F v loc loc (Term v loc)
t -> loc -> F v loc loc (Term v loc) -> Term v loc
forall (f :: * -> *) v a.
(Foldable f, Ord v) =>
a -> f (Term f v a) -> Term f v a
ABT.tm loc
ann F v loc loc (Term v loc)
t

--------------------------------------------------------------------------------
-- Constraints arising from Decls
--------------------------------------------------------------------------------

-- | Generate kind constraints for a mutally recursive component of
-- decls
declComponentConstraints ::
  forall v loc.
  (Var v, Ord loc) =>
  [(Reference, Decl v loc)] ->
  Gen v loc [GeneratedConstraint v loc]
declComponentConstraints :: forall v loc.
(Var v, Ord loc) =>
[(TypeReference, Decl v loc)]
-> Gen v loc [GeneratedConstraint v loc]
declComponentConstraints [(TypeReference, Decl v loc)]
decls = TreeWalk -> ConstraintTree v loc -> [GeneratedConstraint v loc]
forall v loc.
TreeWalk -> ConstraintTree v loc -> [GeneratedConstraint v loc]
flatten TreeWalk
bottomUp (ConstraintTree v loc -> [GeneratedConstraint v loc])
-> Gen v loc (ConstraintTree v loc)
-> Gen v loc [GeneratedConstraint v loc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(TypeReference, Decl v loc)] -> Gen v loc (ConstraintTree v loc)
forall v loc.
(Var v, Ord loc) =>
[(TypeReference, Decl v loc)] -> Gen v loc (ConstraintTree v loc)
declComponentConstraintTree [(TypeReference, Decl v loc)]
decls

declComponentConstraintTree ::
  forall v loc.
  (Var v, Ord loc) =>
  [(Reference, Decl v loc)] ->
  Gen v loc (ConstraintTree v loc)
declComponentConstraintTree :: forall v loc.
(Var v, Ord loc) =>
[(TypeReference, Decl v loc)] -> Gen v loc (ConstraintTree v loc)
declComponentConstraintTree [(TypeReference, Decl v loc)]
decls = do
  [(TypeReference, Decl v loc, UVar v loc)]
decls <- [(TypeReference, Decl v loc)]
-> ((TypeReference, Decl v loc)
    -> Gen v loc (TypeReference, Decl v loc, UVar v loc))
-> Gen v loc [(TypeReference, Decl v loc, UVar v loc)]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for [(TypeReference, Decl v loc)]
decls \(TypeReference
ref, Decl v loc
decl) -> do
    -- Add a kind variable for every datatype
    UVar v loc
declKind <- Type v loc -> Gen v loc (UVar v loc)
forall v loc. Var v => Type v loc -> Gen v loc (UVar v loc)
pushType (loc -> TypeReference -> Type v loc
forall v a. Ord v => a -> TypeReference -> Type v a
Type.ref (DataDeclaration v loc -> loc
forall v a. DataDeclaration v a -> a
DD.annotation (DataDeclaration v loc -> loc) -> DataDeclaration v loc -> loc
forall a b. (a -> b) -> a -> b
$ Decl v loc -> DataDeclaration v loc
forall v a. Decl v a -> DataDeclaration v a
asDataDecl Decl v loc
decl) TypeReference
ref)
    pure (TypeReference
ref, Decl v loc
decl, UVar v loc
declKind)
  ([ConstraintTree v loc]
declConstraints, [ConstraintTree v loc]
constructorConstraints) <-
    [(ConstraintTree v loc, ConstraintTree v loc)]
-> ([ConstraintTree v loc], [ConstraintTree v loc])
forall a b. [(a, b)] -> ([a], [b])
unzip ([(ConstraintTree v loc, ConstraintTree v loc)]
 -> ([ConstraintTree v loc], [ConstraintTree v loc]))
-> Gen v loc [(ConstraintTree v loc, ConstraintTree v loc)]
-> Gen v loc ([ConstraintTree v loc], [ConstraintTree v loc])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(TypeReference, Decl v loc, UVar v loc)]
-> ((TypeReference, Decl v loc, UVar v loc)
    -> Gen v loc (ConstraintTree v loc, ConstraintTree v loc))
-> Gen v loc [(ConstraintTree v loc, ConstraintTree v loc)]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for [(TypeReference, Decl v loc, UVar v loc)]
decls \(TypeReference
ref, Decl v loc
decl, UVar v loc
declKind) -> do
      let declAnn :: loc
declAnn = DataDeclaration v loc -> loc
forall v a. DataDeclaration v a -> a
DD.annotation (DataDeclaration v loc -> loc) -> DataDeclaration v loc -> loc
forall a b. (a -> b) -> a -> b
$ Decl v loc -> DataDeclaration v loc
forall v a. Decl v a -> DataDeclaration v a
asDataDecl Decl v loc
decl
      let declType :: Type v loc
declType = loc -> TypeReference -> Type v loc
forall v a. Ord v => a -> TypeReference -> Type v a
Type.ref loc
declAnn TypeReference
ref
      -- Unify the datatype with @k_1 -> ... -> k_n -> *@ where @n@ is
      -- the number of type parameters
      let tyVars :: [Type v loc]
tyVars = (v -> Type v loc) -> [v] -> [Type v loc]
forall a b. (a -> b) -> [a] -> [b]
map (\v
tyVar -> loc -> v -> Type v loc
forall v a. Ord v => a -> v -> Type v a
Type.var loc
declAnn v
tyVar) (DataDeclaration v loc -> [v]
forall v a. DataDeclaration v a -> [v]
DD.bound (DataDeclaration v loc -> [v]) -> DataDeclaration v loc -> [v]
forall a b. (a -> b) -> a -> b
$ Decl v loc -> DataDeclaration v loc
forall v a. Decl v a -> DataDeclaration v a
asDataDecl Decl v loc
decl)
      [(UVar v loc, Type v loc)]
tyvarKinds <- [Type v loc]
-> (Type v loc -> Gen v loc (UVar v loc, Type v loc))
-> Gen v loc [(UVar v loc, Type v loc)]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for [Type v loc]
tyVars \Type v loc
tyVar -> do
        -- it would be nice to annotate these type vars with their
        -- precise location, but that information doesn't seem to be
        -- available via "DataDeclaration", so we currently settle for
        -- the whole decl annotation.
        UVar v loc
k <- Type v loc -> Gen v loc (UVar v loc)
forall v loc. Var v => Type v loc -> Gen v loc (UVar v loc)
freshVar Type v loc
tyVar
        pure (UVar v loc
k, Type v loc
tyVar)

      let tyvarKindsOnly :: [UVar v loc]
tyvarKindsOnly = ((UVar v loc, Type v loc) -> UVar v loc)
-> [(UVar v loc, Type v loc)] -> [UVar v loc]
forall a b. (a -> b) -> [a] -> [b]
map (UVar v loc, Type v loc) -> UVar v loc
forall a b. (a, b) -> a
fst [(UVar v loc, Type v loc)]
tyvarKinds
      ConstraintTree v loc
constructorConstraints <-
        [ConstraintTree v loc] -> ConstraintTree v loc
forall v loc. [ConstraintTree v loc] -> ConstraintTree v loc
Node ([ConstraintTree v loc] -> ConstraintTree v loc)
-> Gen v loc [ConstraintTree v loc]
-> Gen v loc (ConstraintTree v loc)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(loc, v, Type v loc)]
-> ((loc, v, Type v loc) -> Gen v loc (ConstraintTree v loc))
-> Gen v loc [ConstraintTree v loc]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for (DataDeclaration v loc -> [(loc, v, Type v loc)]
forall v a. DataDeclaration v a -> [(a, v, Type v a)]
DD.constructors' (DataDeclaration v loc -> [(loc, v, Type v loc)])
-> DataDeclaration v loc -> [(loc, v, Type v loc)]
forall a b. (a -> b) -> a -> b
$ Decl v loc -> DataDeclaration v loc
forall v a. Decl v a -> DataDeclaration v a
asDataDecl Decl v loc
decl) \(loc
constructorAnn, v
_, Type v loc
constructorType) -> do
          Type v loc
-> [UVar v loc]
-> Type v loc
-> (Type v loc -> Gen v loc (ConstraintTree v loc))
-> Gen v loc (ConstraintTree v loc)
forall v loc.
(Var v, Ord loc) =>
Type v loc
-> [UVar v loc]
-> Type v loc
-> (Type v loc -> Gen v loc (ConstraintTree v loc))
-> Gen v loc (ConstraintTree v loc)
withInstantiatedConstructorType Type v loc
declType [UVar v loc]
tyvarKindsOnly Type v loc
constructorType \Type v loc
constructorType -> do
            UVar v loc
constructorKind <- Type v loc -> Gen v loc (UVar v loc)
forall v loc. Var v => Type v loc -> Gen v loc (UVar v loc)
freshVar Type v loc
constructorType
            ConstraintTree v loc
ct <- UVar v loc -> Type v loc -> Gen v loc (ConstraintTree v loc)
forall v loc.
(Var v, Ord loc) =>
UVar v loc -> Type v loc -> Gen v loc (ConstraintTree v loc)
typeConstraintTree UVar v loc
constructorKind Type v loc
constructorType
            pure $ GeneratedConstraint v loc
-> ConstraintTree v loc -> ConstraintTree v loc
forall v loc.
GeneratedConstraint v loc
-> ConstraintTree v loc -> ConstraintTree v loc
ParentConstraint (UVar v loc -> Provenance v loc -> GeneratedConstraint v loc
forall uv v loc (typeProv :: * -> * -> *).
uv -> typeProv v loc -> Constraint uv v loc typeProv
IsType UVar v loc
constructorKind (ConstraintContext v loc -> loc -> Provenance v loc
forall v loc. ConstraintContext v loc -> loc -> Provenance v loc
Provenance ConstraintContext v loc
forall v loc. ConstraintContext v loc
DeclDefinition loc
constructorAnn)) ConstraintTree v loc
ct

      (UVar v loc
fullyAppliedKind, Type v loc
_fullyAppliedType, ConstraintTree v loc
declConstraints) <-
        let phi :: (UVar v loc, Type v loc, ConstraintTree v loc)
-> (UVar v loc, Type v loc)
-> Gen v loc (UVar v loc, Type v loc, ConstraintTree v loc)
phi (UVar v loc
dk, Type v loc
dt, ConstraintTree v loc
cts) (UVar v loc
ak, Type v loc
at) = do
              -- introduce a kind uvar for each app node
              let t' :: Type v loc
t' = loc -> Type v loc -> Type v loc -> Type v loc
forall v a. Ord v => a -> Type v a -> Type v a -> Type v a
Type.app loc
declAnn Type v loc
dt Type v loc
at
              UVar v loc
v <- Type v loc -> Gen v loc (UVar v loc)
forall v loc. Var v => Type v loc -> Gen v loc (UVar v loc)
freshVar Type v loc
t'
              let cts' :: ConstraintTree v loc
cts' = GeneratedConstraint v loc
-> ConstraintTree v loc -> ConstraintTree v loc
forall v loc.
GeneratedConstraint v loc
-> ConstraintTree v loc -> ConstraintTree v loc
Constraint (UVar v loc
-> Provenance v loc
-> UVar v loc
-> UVar v loc
-> GeneratedConstraint v loc
forall uv v loc (typeProv :: * -> * -> *).
uv -> Provenance v loc -> uv -> uv -> Constraint uv v loc typeProv
IsArr UVar v loc
dk (ConstraintContext v loc -> loc -> Provenance v loc
forall v loc. ConstraintContext v loc -> loc -> Provenance v loc
Provenance ConstraintContext v loc
forall v loc. ConstraintContext v loc
DeclDefinition loc
declAnn) UVar v loc
ak UVar v loc
v) ConstraintTree v loc
cts
              (UVar v loc, Type v loc, ConstraintTree v loc)
-> Gen v loc (UVar v loc, Type v loc, ConstraintTree v loc)
forall a. a -> Gen v loc a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (UVar v loc
v, Type v loc
t', ConstraintTree v loc
cts')
         in ((UVar v loc, Type v loc, ConstraintTree v loc)
 -> (UVar v loc, Type v loc)
 -> Gen v loc (UVar v loc, Type v loc, ConstraintTree v loc))
-> (UVar v loc, Type v loc, ConstraintTree v loc)
-> [(UVar v loc, Type v loc)]
-> Gen v loc (UVar v loc, Type v loc, ConstraintTree v loc)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldlM (UVar v loc, Type v loc, ConstraintTree v loc)
-> (UVar v loc, Type v loc)
-> Gen v loc (UVar v loc, Type v loc, ConstraintTree v loc)
phi (UVar v loc
declKind, Type v loc
declType, [ConstraintTree v loc] -> ConstraintTree v loc
forall v loc. [ConstraintTree v loc] -> ConstraintTree v loc
Node []) [(UVar v loc, Type v loc)]
tyvarKinds

      let finalDeclConstraints :: ConstraintTree v loc
finalDeclConstraints = case Decl v loc
decl of
            Left EffectDeclaration v loc
_effectDecl -> GeneratedConstraint v loc
-> ConstraintTree v loc -> ConstraintTree v loc
forall v loc.
GeneratedConstraint v loc
-> ConstraintTree v loc -> ConstraintTree v loc
Constraint (UVar v loc -> Provenance v loc -> GeneratedConstraint v loc
forall uv v loc (typeProv :: * -> * -> *).
uv -> Provenance v loc -> Constraint uv v loc typeProv
IsAbility UVar v loc
fullyAppliedKind (ConstraintContext v loc -> loc -> Provenance v loc
forall v loc. ConstraintContext v loc -> loc -> Provenance v loc
Provenance ConstraintContext v loc
forall v loc. ConstraintContext v loc
DeclDefinition loc
declAnn)) ConstraintTree v loc
declConstraints
            Right DataDeclaration v loc
_dataDecl -> GeneratedConstraint v loc
-> ConstraintTree v loc -> ConstraintTree v loc
forall v loc.
GeneratedConstraint v loc
-> ConstraintTree v loc -> ConstraintTree v loc
Constraint (UVar v loc -> Provenance v loc -> GeneratedConstraint v loc
forall uv v loc (typeProv :: * -> * -> *).
uv -> typeProv v loc -> Constraint uv v loc typeProv
IsType UVar v loc
fullyAppliedKind (ConstraintContext v loc -> loc -> Provenance v loc
forall v loc. ConstraintContext v loc -> loc -> Provenance v loc
Provenance ConstraintContext v loc
forall v loc. ConstraintContext v loc
DeclDefinition loc
declAnn)) ConstraintTree v loc
declConstraints
      pure (ConstraintTree v loc
finalDeclConstraints, ConstraintTree v loc
constructorConstraints)
  ConstraintTree v loc -> Gen v loc (ConstraintTree v loc)
forall a. a -> Gen v loc a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([ConstraintTree v loc] -> ConstraintTree v loc
forall v loc. [ConstraintTree v loc] -> ConstraintTree v loc
Node [ConstraintTree v loc]
declConstraints ConstraintTree v loc
-> ConstraintTree v loc -> ConstraintTree v loc
forall v loc.
ConstraintTree v loc
-> ConstraintTree v loc -> ConstraintTree v loc
`StrictOrder` [ConstraintTree v loc] -> ConstraintTree v loc
forall v loc. [ConstraintTree v loc] -> ConstraintTree v loc
Node [ConstraintTree v loc]
constructorConstraints)

-- | This is a helper to unify the kind constraints on type variables
-- across a decl's constructors.
--
-- With a decl like
--
-- @
-- unique type T a = C0 Nat a | C1 (a Nat)
-- @
--
-- @C0@ will have type @forall a. Nat -> a -> T a@ and @C1@ will have
-- type @forall a. (a Nat) -> T a@. We must unify the kind constraints
-- that the two constructors make on @a@ in order to determine the
-- kind of @a@ (or observe that there are contradictory
-- constraints). In this example @C0@ constrains @a@ to be of type *
-- because it is applied to the arrow type, whereas @C1@ constrains
-- @a@ to be of kind * -> * since it is applied to a Nat.
--
-- We unify these variables by instantiating the outermost foralls
-- with fresh kind variables, then follow any arrows to find the
-- result type which must have type @T b@ for some b, then unify @b@
-- with some kind variable representing the unification of @a@ for
-- each constructor.
withInstantiatedConstructorType ::
  forall v loc.
  (Var v, Ord loc) =>
  Type.Type v loc ->
  [UVar v loc] ->
  Type.Type v loc ->
  (Type.Type v loc -> Gen v loc (ConstraintTree v loc)) ->
  Gen v loc (ConstraintTree v loc)
withInstantiatedConstructorType :: forall v loc.
(Var v, Ord loc) =>
Type v loc
-> [UVar v loc]
-> Type v loc
-> (Type v loc -> Gen v loc (ConstraintTree v loc))
-> Gen v loc (ConstraintTree v loc)
withInstantiatedConstructorType Type v loc
declType [UVar v loc]
tyParams0 Type v loc
constructorType0 Type v loc -> Gen v loc (ConstraintTree v loc)
k =
  let goForall :: Type v loc -> Gen v loc (ConstraintTree v loc)
goForall Type v loc
constructorType = case Type v loc
constructorType of
        ABT.Tm' (Type.Forall ABT.Term {loc
annotation :: forall (f :: * -> *) v a. Term f v a -> a
annotation :: loc
annotation, out :: forall (f :: * -> *) v a. Term f v a -> ABT f v (Term f v a)
out = ABT.Abs v
x Type v loc
t}) -> do
          Type v loc
-> (UVar v loc -> Gen v loc (ConstraintTree v loc))
-> Gen v loc (ConstraintTree v loc)
forall v loc r.
Var v =>
Type v loc -> (UVar v loc -> Gen v loc r) -> Gen v loc r
scopedType (loc -> v -> Type v loc
forall v a. Ord v => a -> v -> Type v a
Type.var loc
annotation v
x) \UVar v loc
_ -> do
            Type v loc -> Gen v loc (ConstraintTree v loc)
goForall Type v loc
t
        Type v loc
_ -> do
          [GeneratedConstraint v loc]
cs <- Type v loc -> Gen v loc [GeneratedConstraint v loc]
goArrow Type v loc
constructorType
          ConstraintTree v loc
rest <- Type v loc -> Gen v loc (ConstraintTree v loc)
k Type v loc
constructorType
          pure $ ConstraintTree v loc
-> ConstraintTree v loc -> ConstraintTree v loc
forall v loc.
ConstraintTree v loc
-> ConstraintTree v loc -> ConstraintTree v loc
StrictOrder ((GeneratedConstraint v loc
 -> ConstraintTree v loc -> ConstraintTree v loc)
-> ConstraintTree v loc
-> [GeneratedConstraint v loc]
-> ConstraintTree v loc
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr GeneratedConstraint v loc
-> ConstraintTree v loc -> ConstraintTree v loc
forall v loc.
GeneratedConstraint v loc
-> ConstraintTree v loc -> ConstraintTree v loc
Constraint ([ConstraintTree v loc] -> ConstraintTree v loc
forall v loc. [ConstraintTree v loc] -> ConstraintTree v loc
Node []) [GeneratedConstraint v loc]
cs) ConstraintTree v loc
rest

      goArrow :: Type.Type v loc -> Gen v loc [GeneratedConstraint v loc]
      goArrow :: Type v loc -> Gen v loc [GeneratedConstraint v loc]
goArrow = \case
        Type.Arrow' Type v loc
_ Type v loc
o -> Type v loc -> Gen v loc [GeneratedConstraint v loc]
goArrow Type v loc
o
        Type.Effect' [Type v loc]
es Type v loc
_ -> [Type v loc] -> Gen v loc [GeneratedConstraint v loc]
goEffs [Type v loc]
es
        resultTyp :: Type v loc
resultTyp@(Type.Apps' Type v loc
f [Type v loc]
xs)
          | Type v loc
f Type v loc -> Type v loc -> Bool
forall a. Eq a => a -> a -> Bool
== Type v loc
declType -> Type v loc -> [Type v loc] -> Gen v loc [GeneratedConstraint v loc]
unifyVars Type v loc
resultTyp [Type v loc]
xs
        Type v loc
f | Type v loc
f Type v loc -> Type v loc -> Bool
forall a. Eq a => a -> a -> Bool
== Type v loc
declType -> [GeneratedConstraint v loc]
-> Gen v loc [GeneratedConstraint v loc]
forall a. a -> Gen v loc a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
        Type v loc
resultTyp -> [Char] -> Gen v loc [GeneratedConstraint v loc]
forall a. HasCallStack => [Char] -> a
error ([Char]
"[goArrow] unexpected result type: " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> Type v loc -> [Char]
forall a. Show a => a -> [Char]
show Type v loc
resultTyp)

      goEffs :: [Type v loc] -> Gen v loc [GeneratedConstraint v loc]
goEffs = \case
        [] -> [Char] -> Gen v loc [GeneratedConstraint v loc]
forall a. HasCallStack => [Char] -> a
error ([Char]
"[goEffs] couldn't find the expected ability: " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> Type v loc -> [Char]
forall a. Show a => a -> [Char]
show Type v loc
declType)
        Type v loc
e : [Type v loc]
es
          | Type v loc
e Type v loc -> Type v loc -> Bool
forall a. Eq a => a -> a -> Bool
== Type v loc
declType -> [GeneratedConstraint v loc]
-> Gen v loc [GeneratedConstraint v loc]
forall a. a -> Gen v loc a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
          | Type.Apps' Type v loc
f [Type v loc]
xs <- Type v loc
e,
            Type v loc
f Type v loc -> Type v loc -> Bool
forall a. Eq a => a -> a -> Bool
== Type v loc
declType ->
              Type v loc -> [Type v loc] -> Gen v loc [GeneratedConstraint v loc]
unifyVars Type v loc
e [Type v loc]
xs
          | Bool
otherwise -> [Type v loc] -> Gen v loc [GeneratedConstraint v loc]
goEffs [Type v loc]
es

      unifyVars :: Type.Type v loc -> [Type.Type v loc] -> Gen v loc [GeneratedConstraint v loc]
      unifyVars :: Type v loc -> [Type v loc] -> Gen v loc [GeneratedConstraint v loc]
unifyVars Type v loc
typ [Type v loc]
vs = [(Type v loc, UVar v loc)]
-> ((Type v loc, UVar v loc)
    -> Gen v loc (GeneratedConstraint v loc))
-> Gen v loc [GeneratedConstraint v loc]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for ([Type v loc] -> [UVar v loc] -> [(Type v loc, UVar v loc)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Type v loc]
vs [UVar v loc]
tyParams0) \(Type v loc
v, UVar v loc
tp) -> do
        Type v loc -> Gen v loc (Maybe (UVar v loc))
forall v loc. Var v => Type v loc -> Gen v loc (Maybe (UVar v loc))
lookupType Type v loc
v Gen v loc (Maybe (UVar v loc))
-> (Maybe (UVar v loc) -> Gen v loc (GeneratedConstraint v loc))
-> Gen v loc (GeneratedConstraint v loc)
forall a b. Gen v loc a -> (a -> Gen v loc b) -> Gen v loc b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
          Maybe (UVar v loc)
Nothing -> [Char] -> Gen v loc (GeneratedConstraint v loc)
forall a. HasCallStack => [Char] -> a
error ([Char]
"[unifyVars] unknown type in decl result: " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> Type v loc -> [Char]
forall a. Show a => a -> [Char]
show Type v loc
v)
          Just UVar v loc
x ->
            GeneratedConstraint v loc -> Gen v loc (GeneratedConstraint v loc)
forall a. a -> Gen v loc a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Provenance v loc
-> UVar v loc -> UVar v loc -> GeneratedConstraint v loc
forall uv v loc (typeProv :: * -> * -> *).
Provenance v loc -> uv -> uv -> Constraint uv v loc typeProv
Unify (ConstraintContext v loc -> loc -> Provenance v loc
forall v loc. ConstraintContext v loc -> loc -> Provenance v loc
Provenance ConstraintContext v loc
forall v loc. ConstraintContext v loc
DeclDefinition (Type v loc -> loc
forall (f :: * -> *) v a. Term f v a -> a
ABT.annotation Type v loc
typ)) UVar v loc
x UVar v loc
tp)
   in Type v loc -> Gen v loc (ConstraintTree v loc)
goForall Type v loc
constructorType0

--------------------------------------------------------------------------------
-- Constraints on builtins
--------------------------------------------------------------------------------

-- | Constraints on language builtins, used to initialize the kind
-- inference state ('Unison.KindInference.Solve.initialState')
builtinConstraints :: forall v loc. (Ord loc, BuiltinAnnotation loc, Var v) => Gen v loc [GeneratedConstraint v loc]
builtinConstraints :: forall v loc.
(Ord loc, BuiltinAnnotation loc, Var v) =>
Gen v loc [GeneratedConstraint v loc]
builtinConstraints = TreeWalk -> ConstraintTree v loc -> [GeneratedConstraint v loc]
forall v loc.
TreeWalk -> ConstraintTree v loc -> [GeneratedConstraint v loc]
flatten TreeWalk
bottomUp (ConstraintTree v loc -> [GeneratedConstraint v loc])
-> Gen v loc (ConstraintTree v loc)
-> Gen v loc [GeneratedConstraint v loc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen v loc (ConstraintTree v loc)
forall v loc.
(Ord loc, BuiltinAnnotation loc, Var v) =>
Gen v loc (ConstraintTree v loc)
builtinConstraintTree

-- | Kind constraints for builtin types
builtinConstraintTree :: forall v loc. (Ord loc, BuiltinAnnotation loc, Var v) => Gen v loc (ConstraintTree v loc)
builtinConstraintTree :: forall v loc.
(Ord loc, BuiltinAnnotation loc, Var v) =>
Gen v loc (ConstraintTree v loc)
builtinConstraintTree =
  [Gen v loc [ConstraintTree v loc]]
-> Gen v loc (ConstraintTree v loc)
mergeTrees
    [ ((loc -> Type v loc) -> Gen v loc (ConstraintTree v loc))
-> [loc -> Type v loc] -> Gen v loc [ConstraintTree v loc]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse
        (Kind -> (loc -> Type v loc) -> Gen v loc (ConstraintTree v loc)
constrain Kind
Type)
        [ loc -> Type v loc
forall v a. Ord v => a -> Type v a
Type.nat,
          loc -> Type v loc
forall v a. Ord v => a -> Type v a
Type.int,
          loc -> Type v loc
forall v a. Ord v => a -> Type v a
Type.float,
          loc -> Type v loc
forall v a. Ord v => a -> Type v a
Type.boolean,
          loc -> Type v loc
forall v a. Ord v => a -> Type v a
Type.text,
          loc -> Type v loc
forall v a. Ord v => a -> Type v a
Type.char,
          loc -> Type v loc
forall v a. Ord v => a -> Type v a
Type.bytes,
          loc -> Type v loc
forall v a. Ord v => a -> Type v a
Type.any,
          loc -> Type v loc
forall v a. Ord v => a -> Type v a
Type.termLink,
          loc -> Type v loc
forall v a. Ord v => a -> Type v a
Type.typeLink,
          loc -> Type v loc
forall v a. Ord v => a -> Type v a
Type.fileHandle,
          (loc -> TypeReference -> Type v loc)
-> TypeReference -> loc -> Type v loc
forall a b c. (a -> b -> c) -> b -> a -> c
flip loc -> TypeReference -> Type v loc
forall v a. Ord v => a -> TypeReference -> Type v a
Type.ref TypeReference
Type.filePathRef,
          loc -> Type v loc
forall v a. Ord v => a -> Type v a
Type.threadId,
          loc -> Type v loc
forall v a. Ord v => a -> Type v a
Type.socket,
          loc -> Type v loc
forall v a. Ord v => a -> Type v a
Type.udpSocket,
          loc -> Type v loc
forall v a. Ord v => a -> Type v a
Type.udpListenSocket,
          loc -> Type v loc
forall v a. Ord v => a -> Type v a
Type.udpClientSockAddr,
          loc -> Type v loc
forall v a. Ord v => a -> Type v a
Type.processHandle,
          loc -> Type v loc
forall v a. Ord v => a -> Type v a
Type.ibytearrayType,
          (loc -> TypeReference -> Type v loc)
-> TypeReference -> loc -> Type v loc
forall a b c. (a -> b -> c) -> b -> a -> c
flip loc -> TypeReference -> Type v loc
forall v a. Ord v => a -> TypeReference -> Type v a
Type.ref TypeReference
Type.charClassRef,
          (loc -> TypeReference -> Type v loc)
-> TypeReference -> loc -> Type v loc
forall a b c. (a -> b -> c) -> b -> a -> c
flip loc -> TypeReference -> Type v loc
forall v a. Ord v => a -> TypeReference -> Type v a
Type.ref TypeReference
Type.tlsRef,
          (loc -> TypeReference -> Type v loc)
-> TypeReference -> loc -> Type v loc
forall a b c. (a -> b -> c) -> b -> a -> c
flip loc -> TypeReference -> Type v loc
forall v a. Ord v => a -> TypeReference -> Type v a
Type.ref TypeReference
Type.tlsClientConfigRef,
          (loc -> TypeReference -> Type v loc)
-> TypeReference -> loc -> Type v loc
forall a b c. (a -> b -> c) -> b -> a -> c
flip loc -> TypeReference -> Type v loc
forall v a. Ord v => a -> TypeReference -> Type v a
Type.ref TypeReference
Type.tlsServerConfigRef,
          (loc -> TypeReference -> Type v loc)
-> TypeReference -> loc -> Type v loc
forall a b c. (a -> b -> c) -> b -> a -> c
flip loc -> TypeReference -> Type v loc
forall v a. Ord v => a -> TypeReference -> Type v a
Type.ref TypeReference
Type.tlsSignedCertRef,
          (loc -> TypeReference -> Type v loc)
-> TypeReference -> loc -> Type v loc
forall a b c. (a -> b -> c) -> b -> a -> c
flip loc -> TypeReference -> Type v loc
forall v a. Ord v => a -> TypeReference -> Type v a
Type.ref TypeReference
Type.tlsPrivateKeyRef,
          (loc -> TypeReference -> Type v loc)
-> TypeReference -> loc -> Type v loc
forall a b c. (a -> b -> c) -> b -> a -> c
flip loc -> TypeReference -> Type v loc
forall v a. Ord v => a -> TypeReference -> Type v a
Type.ref TypeReference
Type.tlsCipherRef,
          (loc -> TypeReference -> Type v loc)
-> TypeReference -> loc -> Type v loc
forall a b c. (a -> b -> c) -> b -> a -> c
flip loc -> TypeReference -> Type v loc
forall v a. Ord v => a -> TypeReference -> Type v a
Type.ref TypeReference
Type.tlsVersionRef,
          (loc -> TypeReference -> Type v loc)
-> TypeReference -> loc -> Type v loc
forall a b c. (a -> b -> c) -> b -> a -> c
flip loc -> TypeReference -> Type v loc
forall v a. Ord v => a -> TypeReference -> Type v a
Type.ref TypeReference
Type.codeRef,
          (loc -> TypeReference -> Type v loc)
-> TypeReference -> loc -> Type v loc
forall a b c. (a -> b -> c) -> b -> a -> c
flip loc -> TypeReference -> Type v loc
forall v a. Ord v => a -> TypeReference -> Type v a
Type.ref TypeReference
Type.valueRef,
          (loc -> TypeReference -> Type v loc)
-> TypeReference -> loc -> Type v loc
forall a b c. (a -> b -> c) -> b -> a -> c
flip loc -> TypeReference -> Type v loc
forall v a. Ord v => a -> TypeReference -> Type v a
Type.ref TypeReference
Type.timeSpecRef,
          (loc -> TypeReference -> Type v loc)
-> TypeReference -> loc -> Type v loc
forall a b c. (a -> b -> c) -> b -> a -> c
flip loc -> TypeReference -> Type v loc
forall v a. Ord v => a -> TypeReference -> Type v a
Type.ref TypeReference
Type.hashAlgorithmRef
        ],
      ((loc -> Type v loc) -> Gen v loc (ConstraintTree v loc))
-> [loc -> Type v loc] -> Gen v loc [ConstraintTree v loc]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse
        (Kind -> (loc -> Type v loc) -> Gen v loc (ConstraintTree v loc)
constrain (Kind
Type Kind -> Kind -> Kind
:-> Kind
Type))
        [ loc -> Type v loc
forall v a. Ord v => a -> Type v a
Type.list,
          loc -> Type v loc
forall v a. Ord v => a -> Type v a
Type.iarrayType,
          (loc -> TypeReference -> Type v loc)
-> TypeReference -> loc -> Type v loc
forall a b c. (a -> b -> c) -> b -> a -> c
flip loc -> TypeReference -> Type v loc
forall v a. Ord v => a -> TypeReference -> Type v a
Type.ref TypeReference
Type.mvarRef,
          (loc -> TypeReference -> Type v loc)
-> TypeReference -> loc -> Type v loc
forall a b c. (a -> b -> c) -> b -> a -> c
flip loc -> TypeReference -> Type v loc
forall v a. Ord v => a -> TypeReference -> Type v a
Type.ref TypeReference
Type.tvarRef,
          (loc -> TypeReference -> Type v loc)
-> TypeReference -> loc -> Type v loc
forall a b c. (a -> b -> c) -> b -> a -> c
flip loc -> TypeReference -> Type v loc
forall v a. Ord v => a -> TypeReference -> Type v a
Type.ref TypeReference
Type.ticketRef,
          (loc -> TypeReference -> Type v loc)
-> TypeReference -> loc -> Type v loc
forall a b c. (a -> b -> c) -> b -> a -> c
flip loc -> TypeReference -> Type v loc
forall v a. Ord v => a -> TypeReference -> Type v a
Type.ref TypeReference
Type.promiseRef,
          (loc -> TypeReference -> Type v loc)
-> TypeReference -> loc -> Type v loc
forall a b c. (a -> b -> c) -> b -> a -> c
flip loc -> TypeReference -> Type v loc
forall v a. Ord v => a -> TypeReference -> Type v a
Type.ref TypeReference
Type.patternRef
        ],
      ((loc -> Type v loc) -> Gen v loc (ConstraintTree v loc))
-> [loc -> Type v loc] -> Gen v loc [ConstraintTree v loc]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse
        (Kind -> (loc -> Type v loc) -> Gen v loc (ConstraintTree v loc)
constrain Kind
Ability)
        [ loc -> Type v loc
forall v a. Ord v => a -> Type v a
Type.builtinIO,
          (loc -> TypeReference -> Type v loc)
-> TypeReference -> loc -> Type v loc
forall a b c. (a -> b -> c) -> b -> a -> c
flip loc -> TypeReference -> Type v loc
forall v a. Ord v => a -> TypeReference -> Type v a
Type.ref TypeReference
Type.stmRef
        ],
      ((loc -> Type v loc) -> Gen v loc (ConstraintTree v loc))
-> [loc -> Type v loc] -> Gen v loc [ConstraintTree v loc]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse
        (Kind -> (loc -> Type v loc) -> Gen v loc (ConstraintTree v loc)
constrain (Kind
Type Kind -> Kind -> Kind
:-> Kind
Ability))
        [(loc -> TypeReference -> Type v loc)
-> TypeReference -> loc -> Type v loc
forall a b c. (a -> b -> c) -> b -> a -> c
flip loc -> TypeReference -> Type v loc
forall v a. Ord v => a -> TypeReference -> Type v a
Type.ref TypeReference
Type.scopeRef],
      ((loc -> Type v loc) -> Gen v loc (ConstraintTree v loc))
-> [loc -> Type v loc] -> Gen v loc [ConstraintTree v loc]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse
        (Kind -> (loc -> Type v loc) -> Gen v loc (ConstraintTree v loc)
constrain (Kind
Ability Kind -> Kind -> Kind
:-> Kind
Type))
        [loc -> Type v loc
forall v a. Ord v => a -> Type v a
Type.mbytearrayType],
      ((loc -> Type v loc) -> Gen v loc (ConstraintTree v loc))
-> [loc -> Type v loc] -> Gen v loc [ConstraintTree v loc]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse
        (Kind -> (loc -> Type v loc) -> Gen v loc (ConstraintTree v loc)
constrain (Kind
Ability Kind -> Kind -> Kind
:-> Kind
Type Kind -> Kind -> Kind
:-> Kind
Type))
        [loc -> Type v loc
forall v a. Ord v => a -> Type v a
Type.effectType, loc -> Type v loc
forall v a. Ord v => a -> Type v a
Type.marrayType, loc -> Type v loc
forall v a. Ord v => a -> Type v a
Type.refType]
    ]
  where
    mergeTrees :: [Gen v loc [ConstraintTree v loc]] -> Gen v loc (ConstraintTree v loc)
    mergeTrees :: [Gen v loc [ConstraintTree v loc]]
-> Gen v loc (ConstraintTree v loc)
mergeTrees = ([[ConstraintTree v loc]] -> ConstraintTree v loc)
-> Gen v loc [[ConstraintTree v loc]]
-> Gen v loc (ConstraintTree v loc)
forall a b. (a -> b) -> Gen v loc a -> Gen v loc b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([ConstraintTree v loc] -> ConstraintTree v loc
forall v loc. [ConstraintTree v loc] -> ConstraintTree v loc
Node ([ConstraintTree v loc] -> ConstraintTree v loc)
-> ([[ConstraintTree v loc]] -> [ConstraintTree v loc])
-> [[ConstraintTree v loc]]
-> ConstraintTree v loc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[ConstraintTree v loc]] -> [ConstraintTree v loc]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat) (Gen v loc [[ConstraintTree v loc]]
 -> Gen v loc (ConstraintTree v loc))
-> ([Gen v loc [ConstraintTree v loc]]
    -> Gen v loc [[ConstraintTree v loc]])
-> [Gen v loc [ConstraintTree v loc]]
-> Gen v loc (ConstraintTree v loc)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Gen v loc [ConstraintTree v loc]]
-> Gen v loc [[ConstraintTree v loc]]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Monad m => [m a] -> m [a]
sequence

    constrain :: Kind -> (loc -> Type.Type v loc) -> Gen v loc (ConstraintTree v loc)
    constrain :: Kind -> (loc -> Type v loc) -> Gen v loc (ConstraintTree v loc)
constrain Kind
k loc -> Type v loc
t = do
      UVar v loc
kindVar <- Type v loc -> Gen v loc (UVar v loc)
forall v loc. Var v => Type v loc -> Gen v loc (UVar v loc)
pushType (loc -> Type v loc
t loc
forall a. BuiltinAnnotation a => a
builtinAnnotation)
      (GeneratedConstraint v loc
 -> ConstraintTree v loc -> ConstraintTree v loc)
-> ConstraintTree v loc
-> [GeneratedConstraint v loc]
-> ConstraintTree v loc
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr GeneratedConstraint v loc
-> ConstraintTree v loc -> ConstraintTree v loc
forall v loc.
GeneratedConstraint v loc
-> ConstraintTree v loc -> ConstraintTree v loc
Constraint ([ConstraintTree v loc] -> ConstraintTree v loc
forall v loc. [ConstraintTree v loc] -> ConstraintTree v loc
Node []) ([GeneratedConstraint v loc] -> ConstraintTree v loc)
-> Gen v loc [GeneratedConstraint v loc]
-> Gen v loc (ConstraintTree v loc)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Provenance v loc
-> UVar v loc -> Kind -> Gen v loc [GeneratedConstraint v loc]
forall v loc.
Var v =>
Provenance v loc
-> UVar v loc -> Kind -> Gen v loc [GeneratedConstraint v loc]
constrainToKind (ConstraintContext v loc -> loc -> Provenance v loc
forall v loc. ConstraintContext v loc -> loc -> Provenance v loc
Provenance ConstraintContext v loc
forall v loc. ConstraintContext v loc
Builtin loc
forall a. BuiltinAnnotation a => a
builtinAnnotation) UVar v loc
kindVar Kind
k

--------------------------------------------------------------------------------
-- Helpers for constructing constraints
--------------------------------------------------------------------------------

-- | Constrain a @UVar@ to the provided @Kind@
constrainToKind :: (Var v) => Provenance v loc -> UVar v loc -> Kind -> Gen v loc [GeneratedConstraint v loc]
constrainToKind :: forall v loc.
Var v =>
Provenance v loc
-> UVar v loc -> Kind -> Gen v loc [GeneratedConstraint v loc]
constrainToKind Provenance v loc
prov UVar v loc
resultVar0 = (([Constraint (UVar v loc) v loc Provenance]
  -> [Constraint (UVar v loc) v loc Provenance])
 -> [Constraint (UVar v loc) v loc Provenance])
-> Gen
     v
     loc
     ([Constraint (UVar v loc) v loc Provenance]
      -> [Constraint (UVar v loc) v loc Provenance])
-> Gen v loc [Constraint (UVar v loc) v loc Provenance]
forall a b. (a -> b) -> Gen v loc a -> Gen v loc b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (([Constraint (UVar v loc) v loc Provenance]
 -> [Constraint (UVar v loc) v loc Provenance])
-> [Constraint (UVar v loc) v loc Provenance]
-> [Constraint (UVar v loc) v loc Provenance]
forall a b. (a -> b) -> a -> b
$ []) (Gen
   v
   loc
   ([Constraint (UVar v loc) v loc Provenance]
    -> [Constraint (UVar v loc) v loc Provenance])
 -> Gen v loc [Constraint (UVar v loc) v loc Provenance])
-> (Kind
    -> Gen
         v
         loc
         ([Constraint (UVar v loc) v loc Provenance]
          -> [Constraint (UVar v loc) v loc Provenance]))
-> Kind
-> Gen v loc [Constraint (UVar v loc) v loc Provenance]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UVar v loc
-> Kind
-> Gen
     v
     loc
     ([Constraint (UVar v loc) v loc Provenance]
      -> [Constraint (UVar v loc) v loc Provenance])
go UVar v loc
resultVar0
  where
    go :: UVar v loc
-> Kind
-> Gen
     v
     loc
     ([Constraint (UVar v loc) v loc Provenance]
      -> [Constraint (UVar v loc) v loc Provenance])
go UVar v loc
resultVar = \case
      Kind
Type -> do
        ([Constraint (UVar v loc) v loc Provenance]
 -> [Constraint (UVar v loc) v loc Provenance])
-> Gen
     v
     loc
     ([Constraint (UVar v loc) v loc Provenance]
      -> [Constraint (UVar v loc) v loc Provenance])
forall a. a -> Gen v loc a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (UVar v loc
-> Provenance v loc -> Constraint (UVar v loc) v loc Provenance
forall uv v loc (typeProv :: * -> * -> *).
uv -> typeProv v loc -> Constraint uv v loc typeProv
IsType UVar v loc
resultVar Provenance v loc
prov Constraint (UVar v loc) v loc Provenance
-> [Constraint (UVar v loc) v loc Provenance]
-> [Constraint (UVar v loc) v loc Provenance]
forall a. a -> [a] -> [a]
:)
      Kind
Ability -> do
        ([Constraint (UVar v loc) v loc Provenance]
 -> [Constraint (UVar v loc) v loc Provenance])
-> Gen
     v
     loc
     ([Constraint (UVar v loc) v loc Provenance]
      -> [Constraint (UVar v loc) v loc Provenance])
forall a. a -> Gen v loc a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (UVar v loc
-> Provenance v loc -> Constraint (UVar v loc) v loc Provenance
forall uv v loc (typeProv :: * -> * -> *).
uv -> Provenance v loc -> Constraint uv v loc typeProv
IsAbility UVar v loc
resultVar Provenance v loc
prov Constraint (UVar v loc) v loc Provenance
-> [Constraint (UVar v loc) v loc Provenance]
-> [Constraint (UVar v loc) v loc Provenance]
forall a. a -> [a] -> [a]
:)
      Kind
lhs :-> Kind
rhs -> do
        let inputTypeVar :: Type v loc
inputTypeVar = loc -> v -> Type v loc
forall v a. Ord v => a -> v -> Type v a
Type.var (Provenance v loc
prov Provenance v loc -> Getting loc (Provenance v loc) loc -> loc
forall s a. s -> Getting a s a -> a
^. Getting loc (Provenance v loc) loc
forall v loc (f :: * -> *).
Functor f =>
(loc -> f loc) -> Provenance v loc -> f (Provenance v loc)
Provenance.loc) (Set v -> v -> v
forall v. Var v => Set v -> v -> v
freshIn Set v
forall a. Set a
Set.empty (Type -> v
forall v. Var v => Type -> v
typed (Text -> Type
User Text
"a")))
        let outputTypeVar :: Type v loc
outputTypeVar = loc -> v -> Type v loc
forall v a. Ord v => a -> v -> Type v a
Type.var (Provenance v loc
prov Provenance v loc -> Getting loc (Provenance v loc) loc -> loc
forall s a. s -> Getting a s a -> a
^. Getting loc (Provenance v loc) loc
forall v loc (f :: * -> *).
Functor f =>
(loc -> f loc) -> Provenance v loc -> f (Provenance v loc)
Provenance.loc) (Set v -> v -> v
forall v. Var v => Set v -> v -> v
freshIn Set v
forall a. Set a
Set.empty (Type -> v
forall v. Var v => Type -> v
typed (Text -> Type
User Text
"a")))
        UVar v loc
input <- Type v loc -> Gen v loc (UVar v loc)
forall v loc. Var v => Type v loc -> Gen v loc (UVar v loc)
freshVar Type v loc
inputTypeVar
        UVar v loc
output <- Type v loc -> Gen v loc (UVar v loc)
forall v loc. Var v => Type v loc -> Gen v loc (UVar v loc)
freshVar Type v loc
outputTypeVar
        [Constraint (UVar v loc) v loc Provenance]
-> [Constraint (UVar v loc) v loc Provenance]
ctl <- UVar v loc
-> Kind
-> Gen
     v
     loc
     ([Constraint (UVar v loc) v loc Provenance]
      -> [Constraint (UVar v loc) v loc Provenance])
go UVar v loc
input Kind
lhs
        [Constraint (UVar v loc) v loc Provenance]
-> [Constraint (UVar v loc) v loc Provenance]
ctr <- UVar v loc
-> Kind
-> Gen
     v
     loc
     ([Constraint (UVar v loc) v loc Provenance]
      -> [Constraint (UVar v loc) v loc Provenance])
go UVar v loc
output Kind
rhs
        pure ((UVar v loc
-> Provenance v loc
-> UVar v loc
-> UVar v loc
-> Constraint (UVar v loc) v loc Provenance
forall uv v loc (typeProv :: * -> * -> *).
uv -> Provenance v loc -> uv -> uv -> Constraint uv v loc typeProv
IsArr UVar v loc
resultVar Provenance v loc
prov UVar v loc
input UVar v loc
output Constraint (UVar v loc) v loc Provenance
-> [Constraint (UVar v loc) v loc Provenance]
-> [Constraint (UVar v loc) v loc Provenance]
forall a. a -> [a] -> [a]
:) ([Constraint (UVar v loc) v loc Provenance]
 -> [Constraint (UVar v loc) v loc Provenance])
-> ([Constraint (UVar v loc) v loc Provenance]
    -> [Constraint (UVar v loc) v loc Provenance])
-> [Constraint (UVar v loc) v loc Provenance]
-> [Constraint (UVar v loc) v loc Provenance]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Constraint (UVar v loc) v loc Provenance]
-> [Constraint (UVar v loc) v loc Provenance]
ctl ([Constraint (UVar v loc) v loc Provenance]
 -> [Constraint (UVar v loc) v loc Provenance])
-> ([Constraint (UVar v loc) v loc Provenance]
    -> [Constraint (UVar v loc) v loc Provenance])
-> [Constraint (UVar v loc) v loc Provenance]
-> [Constraint (UVar v loc) v loc Provenance]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Constraint (UVar v loc) v loc Provenance]
-> [Constraint (UVar v loc) v loc Provenance]
ctr)

data Kind = Type | Ability | Kind :-> Kind

infixr 9 :->

-- | Convert the 'Unison.Kind' annotation type to our internal 'Kind'
fromUnisonKind :: Unison.Kind -> Kind
fromUnisonKind :: Kind -> Kind
fromUnisonKind = \case
  Kind
Unison.Star -> Kind
Type
  Unison.Arrow Kind
a Kind
b -> Kind -> Kind
fromUnisonKind Kind
a Kind -> Kind -> Kind
:-> Kind -> Kind
fromUnisonKind Kind
b

--------------------------------------------------------------------------------
-- Constraint ordering
--------------------------------------------------------------------------------

-- | The order in which constraints are generated has a great impact
-- on the error observed. To separate the concern of constraint
-- generation and constraint ordering the constraints are generated as
-- a constraint tree, and the flattening of this tree determines the
-- generated constraint order.
data ConstraintTree v loc
  = Node [ConstraintTree v loc]
  | Constraint (GeneratedConstraint v loc) (ConstraintTree v loc)
  | ParentConstraint (GeneratedConstraint v loc) (ConstraintTree v loc)
  | StrictOrder (ConstraintTree v loc) (ConstraintTree v loc)

newtype TreeWalk = TreeWalk (forall a. ([a] -> [a]) -> [([a] -> [a], [a] -> [a])] -> [a] -> [a])

bottomUp :: TreeWalk
bottomUp :: TreeWalk
bottomUp = (forall a.
 ([a] -> [a]) -> [([a] -> [a], [a] -> [a])] -> [a] -> [a])
-> TreeWalk
TreeWalk \[a] -> [a]
down [([a] -> [a], [a] -> [a])]
pairs0 -> (([a] -> [a], [a] -> [a]) -> ([a] -> [a]) -> [a] -> [a])
-> ([a] -> [a]) -> [([a] -> [a], [a] -> [a])] -> [a] -> [a]
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\([a] -> [a]
d, [a] -> [a]
u) [a] -> [a]
b -> [a] -> [a]
d ([a] -> [a]) -> ([a] -> [a]) -> [a] -> [a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [a] -> [a]
u ([a] -> [a]) -> ([a] -> [a]) -> [a] -> [a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [a] -> [a]
b) [a] -> [a]
forall a. a -> a
id [([a] -> [a], [a] -> [a])]
pairs0 ([a] -> [a]) -> ([a] -> [a]) -> [a] -> [a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [a] -> [a]
down

flatten :: TreeWalk -> ConstraintTree v loc -> [GeneratedConstraint v loc]
flatten :: forall v loc.
TreeWalk -> ConstraintTree v loc -> [GeneratedConstraint v loc]
flatten (TreeWalk forall a. ([a] -> [a]) -> [([a] -> [a], [a] -> [a])] -> [a] -> [a]
f) = (([GeneratedConstraint v loc] -> [GeneratedConstraint v loc])
-> [GeneratedConstraint v loc] -> [GeneratedConstraint v loc]
forall a b. (a -> b) -> a -> b
$ []) (([GeneratedConstraint v loc] -> [GeneratedConstraint v loc])
 -> [GeneratedConstraint v loc])
-> (ConstraintTree v loc
    -> [GeneratedConstraint v loc] -> [GeneratedConstraint v loc])
-> ConstraintTree v loc
-> [GeneratedConstraint v loc]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ConstraintTree v loc
-> [GeneratedConstraint v loc] -> [GeneratedConstraint v loc]
forall v loc.
ConstraintTree v loc
-> [GeneratedConstraint v loc] -> [GeneratedConstraint v loc]
flattenTop
  where
    flattenTop :: ConstraintTree v loc -> [GeneratedConstraint v loc] -> [GeneratedConstraint v loc]
    flattenTop :: forall v loc.
ConstraintTree v loc
-> [GeneratedConstraint v loc] -> [GeneratedConstraint v loc]
flattenTop ConstraintTree v loc
t0 =
      ([GeneratedConstraint v loc] -> [GeneratedConstraint v loc])
-> [([GeneratedConstraint v loc] -> [GeneratedConstraint v loc],
     [GeneratedConstraint v loc] -> [GeneratedConstraint v loc])]
-> [GeneratedConstraint v loc]
-> [GeneratedConstraint v loc]
forall a. ([a] -> [a]) -> [([a] -> [a], [a] -> [a])] -> [a] -> [a]
f [GeneratedConstraint v loc] -> [GeneratedConstraint v loc]
forall a. a -> a
id [([GeneratedConstraint v loc] -> [GeneratedConstraint v loc])
-> ConstraintTree v loc
-> ([GeneratedConstraint v loc] -> [GeneratedConstraint v loc],
    [GeneratedConstraint v loc] -> [GeneratedConstraint v loc])
forall v loc.
([GeneratedConstraint v loc] -> [GeneratedConstraint v loc])
-> ConstraintTree v loc
-> ([GeneratedConstraint v loc] -> [GeneratedConstraint v loc],
    [GeneratedConstraint v loc] -> [GeneratedConstraint v loc])
flattenRec [GeneratedConstraint v loc] -> [GeneratedConstraint v loc]
forall a. a -> a
id ConstraintTree v loc
t0]

    flattenRec ::
      ([GeneratedConstraint v loc] -> [GeneratedConstraint v loc]) ->
      ConstraintTree v loc ->
      ([GeneratedConstraint v loc] -> [GeneratedConstraint v loc], [GeneratedConstraint v loc] -> [GeneratedConstraint v loc])
    flattenRec :: forall v loc.
([GeneratedConstraint v loc] -> [GeneratedConstraint v loc])
-> ConstraintTree v loc
-> ([GeneratedConstraint v loc] -> [GeneratedConstraint v loc],
    [GeneratedConstraint v loc] -> [GeneratedConstraint v loc])
flattenRec [GeneratedConstraint v loc] -> [GeneratedConstraint v loc]
down = \case
      Node [ConstraintTree v loc]
cts ->
        let pairs :: [([GeneratedConstraint v loc] -> [GeneratedConstraint v loc],
  [GeneratedConstraint v loc] -> [GeneratedConstraint v loc])]
pairs = (ConstraintTree v loc
 -> ([GeneratedConstraint v loc] -> [GeneratedConstraint v loc],
     [GeneratedConstraint v loc] -> [GeneratedConstraint v loc]))
-> [ConstraintTree v loc]
-> [([GeneratedConstraint v loc] -> [GeneratedConstraint v loc],
     [GeneratedConstraint v loc] -> [GeneratedConstraint v loc])]
forall a b. (a -> b) -> [a] -> [b]
map (([GeneratedConstraint v loc] -> [GeneratedConstraint v loc])
-> ConstraintTree v loc
-> ([GeneratedConstraint v loc] -> [GeneratedConstraint v loc],
    [GeneratedConstraint v loc] -> [GeneratedConstraint v loc])
forall v loc.
([GeneratedConstraint v loc] -> [GeneratedConstraint v loc])
-> ConstraintTree v loc
-> ([GeneratedConstraint v loc] -> [GeneratedConstraint v loc],
    [GeneratedConstraint v loc] -> [GeneratedConstraint v loc])
flattenRec [GeneratedConstraint v loc] -> [GeneratedConstraint v loc]
forall a. a -> a
id) [ConstraintTree v loc]
cts
         in (([GeneratedConstraint v loc] -> [GeneratedConstraint v loc])
-> [([GeneratedConstraint v loc] -> [GeneratedConstraint v loc],
     [GeneratedConstraint v loc] -> [GeneratedConstraint v loc])]
-> [GeneratedConstraint v loc]
-> [GeneratedConstraint v loc]
forall a. ([a] -> [a]) -> [([a] -> [a], [a] -> [a])] -> [a] -> [a]
f [GeneratedConstraint v loc] -> [GeneratedConstraint v loc]
down [([GeneratedConstraint v loc] -> [GeneratedConstraint v loc],
  [GeneratedConstraint v loc] -> [GeneratedConstraint v loc])]
pairs, [GeneratedConstraint v loc] -> [GeneratedConstraint v loc]
forall a. a -> a
id)
      Constraint GeneratedConstraint v loc
c ConstraintTree v loc
ct -> ([GeneratedConstraint v loc] -> [GeneratedConstraint v loc])
-> ConstraintTree v loc
-> ([GeneratedConstraint v loc] -> [GeneratedConstraint v loc],
    [GeneratedConstraint v loc] -> [GeneratedConstraint v loc])
forall v loc.
([GeneratedConstraint v loc] -> [GeneratedConstraint v loc])
-> ConstraintTree v loc
-> ([GeneratedConstraint v loc] -> [GeneratedConstraint v loc],
    [GeneratedConstraint v loc] -> [GeneratedConstraint v loc])
flattenRec ([GeneratedConstraint v loc] -> [GeneratedConstraint v loc]
down ([GeneratedConstraint v loc] -> [GeneratedConstraint v loc])
-> ([GeneratedConstraint v loc] -> [GeneratedConstraint v loc])
-> [GeneratedConstraint v loc]
-> [GeneratedConstraint v loc]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (GeneratedConstraint v loc
c GeneratedConstraint v loc
-> [GeneratedConstraint v loc] -> [GeneratedConstraint v loc]
forall a. a -> [a] -> [a]
:)) ConstraintTree v loc
ct
      ParentConstraint GeneratedConstraint v loc
c ConstraintTree v loc
ct ->
        let ([GeneratedConstraint v loc] -> [GeneratedConstraint v loc]
down', [GeneratedConstraint v loc] -> [GeneratedConstraint v loc]
up) = ([GeneratedConstraint v loc] -> [GeneratedConstraint v loc])
-> ConstraintTree v loc
-> ([GeneratedConstraint v loc] -> [GeneratedConstraint v loc],
    [GeneratedConstraint v loc] -> [GeneratedConstraint v loc])
forall v loc.
([GeneratedConstraint v loc] -> [GeneratedConstraint v loc])
-> ConstraintTree v loc
-> ([GeneratedConstraint v loc] -> [GeneratedConstraint v loc],
    [GeneratedConstraint v loc] -> [GeneratedConstraint v loc])
flattenRec [GeneratedConstraint v loc] -> [GeneratedConstraint v loc]
down ConstraintTree v loc
ct
         in ([GeneratedConstraint v loc] -> [GeneratedConstraint v loc]
down', [GeneratedConstraint v loc] -> [GeneratedConstraint v loc]
up ([GeneratedConstraint v loc] -> [GeneratedConstraint v loc])
-> ([GeneratedConstraint v loc] -> [GeneratedConstraint v loc])
-> [GeneratedConstraint v loc]
-> [GeneratedConstraint v loc]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (GeneratedConstraint v loc
c GeneratedConstraint v loc
-> [GeneratedConstraint v loc] -> [GeneratedConstraint v loc]
forall a. a -> [a] -> [a]
:))
      StrictOrder ConstraintTree v loc
a ConstraintTree v loc
b ->
        let as :: [GeneratedConstraint v loc] -> [GeneratedConstraint v loc]
as = ConstraintTree v loc
-> [GeneratedConstraint v loc] -> [GeneratedConstraint v loc]
forall v loc.
ConstraintTree v loc
-> [GeneratedConstraint v loc] -> [GeneratedConstraint v loc]
flattenTop ConstraintTree v loc
a
            bs :: [GeneratedConstraint v loc] -> [GeneratedConstraint v loc]
bs = ConstraintTree v loc
-> [GeneratedConstraint v loc] -> [GeneratedConstraint v loc]
forall v loc.
ConstraintTree v loc
-> [GeneratedConstraint v loc] -> [GeneratedConstraint v loc]
flattenTop ConstraintTree v loc
b
         in (([GeneratedConstraint v loc] -> [GeneratedConstraint v loc])
-> [([GeneratedConstraint v loc] -> [GeneratedConstraint v loc],
     [GeneratedConstraint v loc] -> [GeneratedConstraint v loc])]
-> [GeneratedConstraint v loc]
-> [GeneratedConstraint v loc]
forall a. ([a] -> [a]) -> [([a] -> [a], [a] -> [a])] -> [a] -> [a]
f [GeneratedConstraint v loc] -> [GeneratedConstraint v loc]
down [([GeneratedConstraint v loc] -> [GeneratedConstraint v loc]
as ([GeneratedConstraint v loc] -> [GeneratedConstraint v loc])
-> ([GeneratedConstraint v loc] -> [GeneratedConstraint v loc])
-> [GeneratedConstraint v loc]
-> [GeneratedConstraint v loc]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [GeneratedConstraint v loc] -> [GeneratedConstraint v loc]
bs, [GeneratedConstraint v loc] -> [GeneratedConstraint v loc]
forall a. a -> a
id)], [GeneratedConstraint v loc] -> [GeneratedConstraint v loc]
forall a. a -> a
id)