{- -----------------------------------------------------------------------------
Copyright 2019-2022,2023 Kevin P. Barry

Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at

    http://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
----------------------------------------------------------------------------- -}

-- Author: Kevin P. Barry [ta0kira@gmail.com]

{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE Safe #-}

module Types.TypeInstance (
  AnyTypeResolver(..),
  CategoryName(..),
  DefinesInstance(..),
  FilterDirection(..),
  GeneralInstance,
  InferredTypeGuess(..),
  InstanceFilters,
  InstanceParams,
  InstanceVariances,
  ParamFilters,
  ParamValues,
  ParamVariances,
  ParamName(..),
  StorageType(..),
  TypeFilter(..),
  TypeInstance(..),
  TypeInstanceOrParam(..),
  TypeResolver(..),
  ValueType(..),
  checkDefinesMatch,
  checkGeneralMatch,
  checkValueAssignment,
  checkValueTypeImmutable,
  checkValueTypeMatch,
  dedupGeneralInstance,
  filterLookup,
  fixTypeParams,
  flipFilter,
  getValueForParam,
  hasInferredParams,
  isDefinesFilter,
  isOptionalValue,
  isRequiresFilter,
  isWeakValue,
  mapTypeGuesses,
  noInferredTypes,
  replaceSelfFilter,
  replaceSelfInstance,
  replaceSelfSingle,
  replaceSelfValueType,
  requiredParam,
  requiredSingleton,
  reverseSelfInstance,
  selfType,
  uncheckedSubFilter,
  uncheckedSubFilters,
  uncheckedSubInstance,
  uncheckedSubSingle,
  uncheckedSubValueType,
  unfixTypeParams,
  validateAssignment,
  validateDefinesInstance,
  validateDefinesVariance,
  validateGeneralInstance,
  validateGeneralInstanceForCall,
  validateInstanceVariance,
  validateTypeInstance,
  validateTypeInstanceForCall,
  validateTypeFilter,
) where

import Control.Monad (when,(>=>))
import Data.List (intercalate)
import qualified Data.Map as Map
import qualified Data.Set as Set

import Base.CompilerError
import Base.GeneralType
import Base.MergeTree
import Base.Mergeable
import Base.Positional
import Types.Variance


type GeneralInstance = GeneralType TypeInstanceOrParam

instance Show GeneralInstance where
  show :: GeneralInstance -> String
show = forall a b.
PreserveMerge a =>
([b] -> b) -> ([b] -> b) -> (T a -> b) -> a -> b
reduceMergeTree [String] -> String
showAny [String] -> String
showAll forall a. Show a => a -> String
show where
    showAny :: [String] -> String
showAny [] = String
"all"
    showAny [String]
ts = String
"[" forall a. [a] -> [a] -> [a]
++ forall a. [a] -> [[a]] -> [a]
intercalate String
"|" [String]
ts forall a. [a] -> [a] -> [a]
++ String
"]"
    showAll :: [String] -> String
showAll [] = String
"any"
    showAll [String]
ts = String
"[" forall a. [a] -> [a] -> [a]
++ forall a. [a] -> [[a]] -> [a]
intercalate String
"&" [String]
ts forall a. [a] -> [a] -> [a]
++ String
"]"

data StorageType =
  WeakValue |
  OptionalValue |
  RequiredValue
  deriving (StorageType -> StorageType -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: StorageType -> StorageType -> Bool
$c/= :: StorageType -> StorageType -> Bool
== :: StorageType -> StorageType -> Bool
$c== :: StorageType -> StorageType -> Bool
Eq,Eq StorageType
StorageType -> StorageType -> Bool
StorageType -> StorageType -> Ordering
StorageType -> StorageType -> StorageType
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: StorageType -> StorageType -> StorageType
$cmin :: StorageType -> StorageType -> StorageType
max :: StorageType -> StorageType -> StorageType
$cmax :: StorageType -> StorageType -> StorageType
>= :: StorageType -> StorageType -> Bool
$c>= :: StorageType -> StorageType -> Bool
> :: StorageType -> StorageType -> Bool
$c> :: StorageType -> StorageType -> Bool
<= :: StorageType -> StorageType -> Bool
$c<= :: StorageType -> StorageType -> Bool
< :: StorageType -> StorageType -> Bool
$c< :: StorageType -> StorageType -> Bool
compare :: StorageType -> StorageType -> Ordering
$ccompare :: StorageType -> StorageType -> Ordering
Ord)

data ValueType =
  ValueType {
    ValueType -> StorageType
vtRequired :: StorageType,
    ValueType -> GeneralInstance
vtType :: GeneralInstance
  }
  deriving (ValueType -> ValueType -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ValueType -> ValueType -> Bool
$c/= :: ValueType -> ValueType -> Bool
== :: ValueType -> ValueType -> Bool
$c== :: ValueType -> ValueType -> Bool
Eq,Eq ValueType
ValueType -> ValueType -> Bool
ValueType -> ValueType -> Ordering
ValueType -> ValueType -> ValueType
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: ValueType -> ValueType -> ValueType
$cmin :: ValueType -> ValueType -> ValueType
max :: ValueType -> ValueType -> ValueType
$cmax :: ValueType -> ValueType -> ValueType
>= :: ValueType -> ValueType -> Bool
$c>= :: ValueType -> ValueType -> Bool
> :: ValueType -> ValueType -> Bool
$c> :: ValueType -> ValueType -> Bool
<= :: ValueType -> ValueType -> Bool
$c<= :: ValueType -> ValueType -> Bool
< :: ValueType -> ValueType -> Bool
$c< :: ValueType -> ValueType -> Bool
compare :: ValueType -> ValueType -> Ordering
$ccompare :: ValueType -> ValueType -> Ordering
Ord)

instance Show ValueType where
  show :: ValueType -> String
show (ValueType StorageType
WeakValue GeneralInstance
t)     = String
"weak " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show GeneralInstance
t
  show (ValueType StorageType
OptionalValue GeneralInstance
t) = String
"optional " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show GeneralInstance
t
  show (ValueType StorageType
RequiredValue GeneralInstance
t) = forall a. Show a => a -> String
show GeneralInstance
t

isWeakValue :: ValueType -> Bool
isWeakValue :: ValueType -> Bool
isWeakValue = (forall a. Eq a => a -> a -> Bool
== StorageType
WeakValue) forall b c a. (b -> c) -> (a -> b) -> a -> c
. ValueType -> StorageType
vtRequired

isOptionalValue :: ValueType -> Bool
isOptionalValue :: ValueType -> Bool
isOptionalValue = (forall a. Eq a => a -> a -> Bool
== StorageType
OptionalValue) forall b c a. (b -> c) -> (a -> b) -> a -> c
. ValueType -> StorageType
vtRequired

requiredSingleton :: CategoryName -> ValueType
requiredSingleton :: CategoryName -> ValueType
requiredSingleton CategoryName
n = StorageType -> GeneralInstance -> ValueType
ValueType StorageType
RequiredValue forall a b. (a -> b) -> a -> b
$ forall a. (Eq a, Ord a) => a -> GeneralType a
singleType forall a b. (a -> b) -> a -> b
$ TypeInstance -> TypeInstanceOrParam
JustTypeInstance forall a b. (a -> b) -> a -> b
$ CategoryName -> InstanceParams -> TypeInstance
TypeInstance CategoryName
n (forall a. [a] -> Positional a
Positional [])

requiredParam :: ParamName -> ValueType
requiredParam :: ParamName -> ValueType
requiredParam ParamName
n = StorageType -> GeneralInstance -> ValueType
ValueType StorageType
RequiredValue forall a b. (a -> b) -> a -> b
$ forall a. (Eq a, Ord a) => a -> GeneralType a
singleType forall a b. (a -> b) -> a -> b
$ Bool -> ParamName -> TypeInstanceOrParam
JustParamName Bool
False ParamName
n

data CategoryName =
  CategoryName {
    CategoryName -> String
tnName :: String
  } |
  BuiltinBool |
  BuiltinChar |
  BuiltinCharBuffer |
  BuiltinInt |
  BuiltinFloat |
  BuiltinString |
  BuiltinPointer |
  BuiltinIdentifier |
  BuiltinFormatted |
  BuiltinOrder |
  BuiltinTestcase |
  CategoryNone

instance Show CategoryName where
  show :: CategoryName -> String
show (CategoryName String
n)  = String
n
  show CategoryName
BuiltinBool       = String
"Bool"
  show CategoryName
BuiltinChar       = String
"Char"
  show CategoryName
BuiltinCharBuffer = String
"CharBuffer"
  show CategoryName
BuiltinInt        = String
"Int"
  show CategoryName
BuiltinFloat      = String
"Float"
  show CategoryName
BuiltinString     = String
"String"
  show CategoryName
BuiltinPointer    = String
"Pointer"
  show CategoryName
BuiltinIdentifier = String
"Identifier"
  show CategoryName
BuiltinFormatted  = String
"Formatted"
  show CategoryName
BuiltinOrder      = String
"Order"
  show CategoryName
BuiltinTestcase   = String
"Testcase"
  show CategoryName
CategoryNone      = String
"(none)"

instance Eq CategoryName where
  CategoryName
c1 == :: CategoryName -> CategoryName -> Bool
== CategoryName
c2 = forall a. Show a => a -> String
show CategoryName
c1 forall a. Eq a => a -> a -> Bool
== forall a. Show a => a -> String
show CategoryName
c2

instance Ord CategoryName where
  CategoryName
c1 <= :: CategoryName -> CategoryName -> Bool
<= CategoryName
c2 = forall a. Show a => a -> String
show CategoryName
c1 forall a. Ord a => a -> a -> Bool
<= forall a. Show a => a -> String
show CategoryName
c2

data ParamName =
  ParamName {
    ParamName -> String
pnName :: String
  } |
  ParamSelf
  deriving (ParamName -> ParamName -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ParamName -> ParamName -> Bool
$c/= :: ParamName -> ParamName -> Bool
== :: ParamName -> ParamName -> Bool
$c== :: ParamName -> ParamName -> Bool
Eq,Eq ParamName
ParamName -> ParamName -> Bool
ParamName -> ParamName -> Ordering
ParamName -> ParamName -> ParamName
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: ParamName -> ParamName -> ParamName
$cmin :: ParamName -> ParamName -> ParamName
max :: ParamName -> ParamName -> ParamName
$cmax :: ParamName -> ParamName -> ParamName
>= :: ParamName -> ParamName -> Bool
$c>= :: ParamName -> ParamName -> Bool
> :: ParamName -> ParamName -> Bool
$c> :: ParamName -> ParamName -> Bool
<= :: ParamName -> ParamName -> Bool
$c<= :: ParamName -> ParamName -> Bool
< :: ParamName -> ParamName -> Bool
$c< :: ParamName -> ParamName -> Bool
compare :: ParamName -> ParamName -> Ordering
$ccompare :: ParamName -> ParamName -> Ordering
Ord)

instance Show ParamName where
  show :: ParamName -> String
show (ParamName String
n) = String
n
  show ParamName
ParamSelf     = String
"#self"

selfType :: GeneralInstance
selfType :: GeneralInstance
selfType = forall a. (Eq a, Ord a) => a -> GeneralType a
singleType forall a b. (a -> b) -> a -> b
$ Bool -> ParamName -> TypeInstanceOrParam
JustParamName Bool
True ParamName
ParamSelf

data TypeInstance =
  TypeInstance {
    TypeInstance -> CategoryName
tiName :: CategoryName,
    TypeInstance -> InstanceParams
tiParams :: InstanceParams
  }
  deriving (TypeInstance -> TypeInstance -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: TypeInstance -> TypeInstance -> Bool
$c/= :: TypeInstance -> TypeInstance -> Bool
== :: TypeInstance -> TypeInstance -> Bool
$c== :: TypeInstance -> TypeInstance -> Bool
Eq,Eq TypeInstance
TypeInstance -> TypeInstance -> Bool
TypeInstance -> TypeInstance -> Ordering
TypeInstance -> TypeInstance -> TypeInstance
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: TypeInstance -> TypeInstance -> TypeInstance
$cmin :: TypeInstance -> TypeInstance -> TypeInstance
max :: TypeInstance -> TypeInstance -> TypeInstance
$cmax :: TypeInstance -> TypeInstance -> TypeInstance
>= :: TypeInstance -> TypeInstance -> Bool
$c>= :: TypeInstance -> TypeInstance -> Bool
> :: TypeInstance -> TypeInstance -> Bool
$c> :: TypeInstance -> TypeInstance -> Bool
<= :: TypeInstance -> TypeInstance -> Bool
$c<= :: TypeInstance -> TypeInstance -> Bool
< :: TypeInstance -> TypeInstance -> Bool
$c< :: TypeInstance -> TypeInstance -> Bool
compare :: TypeInstance -> TypeInstance -> Ordering
$ccompare :: TypeInstance -> TypeInstance -> Ordering
Ord)

instance Show TypeInstance where
  show :: TypeInstance -> String
show (TypeInstance CategoryName
n (Positional [])) = forall a. Show a => a -> String
show CategoryName
n
  show (TypeInstance CategoryName
n (Positional [GeneralInstance]
ts)) =
    forall a. Show a => a -> String
show CategoryName
n forall a. [a] -> [a] -> [a]
++ String
"<" forall a. [a] -> [a] -> [a]
++ forall a. [a] -> [[a]] -> [a]
intercalate String
"," (forall a b. (a -> b) -> [a] -> [b]
map forall a. Show a => a -> String
show [GeneralInstance]
ts) forall a. [a] -> [a] -> [a]
++ String
">"

data DefinesInstance =
  DefinesInstance {
    DefinesInstance -> CategoryName
diName :: CategoryName,
    DefinesInstance -> InstanceParams
diParams :: InstanceParams
  }
  deriving (DefinesInstance -> DefinesInstance -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: DefinesInstance -> DefinesInstance -> Bool
$c/= :: DefinesInstance -> DefinesInstance -> Bool
== :: DefinesInstance -> DefinesInstance -> Bool
$c== :: DefinesInstance -> DefinesInstance -> Bool
Eq,Eq DefinesInstance
DefinesInstance -> DefinesInstance -> Bool
DefinesInstance -> DefinesInstance -> Ordering
DefinesInstance -> DefinesInstance -> DefinesInstance
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: DefinesInstance -> DefinesInstance -> DefinesInstance
$cmin :: DefinesInstance -> DefinesInstance -> DefinesInstance
max :: DefinesInstance -> DefinesInstance -> DefinesInstance
$cmax :: DefinesInstance -> DefinesInstance -> DefinesInstance
>= :: DefinesInstance -> DefinesInstance -> Bool
$c>= :: DefinesInstance -> DefinesInstance -> Bool
> :: DefinesInstance -> DefinesInstance -> Bool
$c> :: DefinesInstance -> DefinesInstance -> Bool
<= :: DefinesInstance -> DefinesInstance -> Bool
$c<= :: DefinesInstance -> DefinesInstance -> Bool
< :: DefinesInstance -> DefinesInstance -> Bool
$c< :: DefinesInstance -> DefinesInstance -> Bool
compare :: DefinesInstance -> DefinesInstance -> Ordering
$ccompare :: DefinesInstance -> DefinesInstance -> Ordering
Ord)

instance Show DefinesInstance where
  show :: DefinesInstance -> String
show (DefinesInstance CategoryName
n (Positional [])) = forall a. Show a => a -> String
show CategoryName
n
  show (DefinesInstance CategoryName
n (Positional [GeneralInstance]
ts)) =
    forall a. Show a => a -> String
show CategoryName
n forall a. [a] -> [a] -> [a]
++ String
"<" forall a. [a] -> [a] -> [a]
++ forall a. [a] -> [[a]] -> [a]
intercalate String
"," (forall a b. (a -> b) -> [a] -> [b]
map forall a. Show a => a -> String
show [GeneralInstance]
ts) forall a. [a] -> [a] -> [a]
++ String
">"

data InferredTypeGuess =
  InferredTypeGuess {
    InferredTypeGuess -> ParamName
itgParam :: ParamName,
    InferredTypeGuess -> GeneralInstance
itgGuess :: GeneralInstance,
    InferredTypeGuess -> Variance
itgVariance :: Variance
  }
  deriving (InferredTypeGuess -> InferredTypeGuess -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: InferredTypeGuess -> InferredTypeGuess -> Bool
$c/= :: InferredTypeGuess -> InferredTypeGuess -> Bool
== :: InferredTypeGuess -> InferredTypeGuess -> Bool
$c== :: InferredTypeGuess -> InferredTypeGuess -> Bool
Eq,Eq InferredTypeGuess
InferredTypeGuess -> InferredTypeGuess -> Bool
InferredTypeGuess -> InferredTypeGuess -> Ordering
InferredTypeGuess -> InferredTypeGuess -> InferredTypeGuess
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: InferredTypeGuess -> InferredTypeGuess -> InferredTypeGuess
$cmin :: InferredTypeGuess -> InferredTypeGuess -> InferredTypeGuess
max :: InferredTypeGuess -> InferredTypeGuess -> InferredTypeGuess
$cmax :: InferredTypeGuess -> InferredTypeGuess -> InferredTypeGuess
>= :: InferredTypeGuess -> InferredTypeGuess -> Bool
$c>= :: InferredTypeGuess -> InferredTypeGuess -> Bool
> :: InferredTypeGuess -> InferredTypeGuess -> Bool
$c> :: InferredTypeGuess -> InferredTypeGuess -> Bool
<= :: InferredTypeGuess -> InferredTypeGuess -> Bool
$c<= :: InferredTypeGuess -> InferredTypeGuess -> Bool
< :: InferredTypeGuess -> InferredTypeGuess -> Bool
$c< :: InferredTypeGuess -> InferredTypeGuess -> Bool
compare :: InferredTypeGuess -> InferredTypeGuess -> Ordering
$ccompare :: InferredTypeGuess -> InferredTypeGuess -> Ordering
Ord)

instance Show InferredTypeGuess where
  show :: InferredTypeGuess -> String
show (InferredTypeGuess ParamName
n GeneralInstance
g Variance
v) = forall a. Show a => a -> String
show ParamName
n forall a. [a] -> [a] -> [a]
++ String
" = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show GeneralInstance
g forall a. [a] -> [a] -> [a]
++ String
" (" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Variance
v forall a. [a] -> [a] -> [a]
++ String
")"

data TypeInstanceOrParam =
  JustTypeInstance {
    TypeInstanceOrParam -> TypeInstance
jtiType :: TypeInstance
  } |
  JustParamName {
    TypeInstanceOrParam -> Bool
jpnFixed :: Bool,
    TypeInstanceOrParam -> ParamName
jpnName :: ParamName
  } |
  JustInferredType {
    TypeInstanceOrParam -> ParamName
jitParam :: ParamName
  }
  deriving (TypeInstanceOrParam -> TypeInstanceOrParam -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: TypeInstanceOrParam -> TypeInstanceOrParam -> Bool
$c/= :: TypeInstanceOrParam -> TypeInstanceOrParam -> Bool
== :: TypeInstanceOrParam -> TypeInstanceOrParam -> Bool
$c== :: TypeInstanceOrParam -> TypeInstanceOrParam -> Bool
Eq,Eq TypeInstanceOrParam
TypeInstanceOrParam -> TypeInstanceOrParam -> Bool
TypeInstanceOrParam -> TypeInstanceOrParam -> Ordering
TypeInstanceOrParam -> TypeInstanceOrParam -> TypeInstanceOrParam
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: TypeInstanceOrParam -> TypeInstanceOrParam -> TypeInstanceOrParam
$cmin :: TypeInstanceOrParam -> TypeInstanceOrParam -> TypeInstanceOrParam
max :: TypeInstanceOrParam -> TypeInstanceOrParam -> TypeInstanceOrParam
$cmax :: TypeInstanceOrParam -> TypeInstanceOrParam -> TypeInstanceOrParam
>= :: TypeInstanceOrParam -> TypeInstanceOrParam -> Bool
$c>= :: TypeInstanceOrParam -> TypeInstanceOrParam -> Bool
> :: TypeInstanceOrParam -> TypeInstanceOrParam -> Bool
$c> :: TypeInstanceOrParam -> TypeInstanceOrParam -> Bool
<= :: TypeInstanceOrParam -> TypeInstanceOrParam -> Bool
$c<= :: TypeInstanceOrParam -> TypeInstanceOrParam -> Bool
< :: TypeInstanceOrParam -> TypeInstanceOrParam -> Bool
$c< :: TypeInstanceOrParam -> TypeInstanceOrParam -> Bool
compare :: TypeInstanceOrParam -> TypeInstanceOrParam -> Ordering
$ccompare :: TypeInstanceOrParam -> TypeInstanceOrParam -> Ordering
Ord)

instance Show TypeInstanceOrParam where
  show :: TypeInstanceOrParam -> String
show (JustTypeInstance TypeInstance
t)   = forall a. Show a => a -> String
show TypeInstance
t
  show (JustParamName Bool
True ParamName
n) = forall a. Show a => a -> String
show ParamName
n forall a. [a] -> [a] -> [a]
++ String
"/*fixed*/"
  show (JustParamName Bool
_ ParamName
n)    = forall a. Show a => a -> String
show ParamName
n
  show (JustInferredType ParamName
n)   = forall a. Show a => a -> String
show ParamName
n forall a. [a] -> [a] -> [a]
++ String
"/*inferred*/"

data FilterDirection =
  FilterRequires |
  FilterAllows
  deriving (FilterDirection -> FilterDirection -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: FilterDirection -> FilterDirection -> Bool
$c/= :: FilterDirection -> FilterDirection -> Bool
== :: FilterDirection -> FilterDirection -> Bool
$c== :: FilterDirection -> FilterDirection -> Bool
Eq,Eq FilterDirection
FilterDirection -> FilterDirection -> Bool
FilterDirection -> FilterDirection -> Ordering
FilterDirection -> FilterDirection -> FilterDirection
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: FilterDirection -> FilterDirection -> FilterDirection
$cmin :: FilterDirection -> FilterDirection -> FilterDirection
max :: FilterDirection -> FilterDirection -> FilterDirection
$cmax :: FilterDirection -> FilterDirection -> FilterDirection
>= :: FilterDirection -> FilterDirection -> Bool
$c>= :: FilterDirection -> FilterDirection -> Bool
> :: FilterDirection -> FilterDirection -> Bool
$c> :: FilterDirection -> FilterDirection -> Bool
<= :: FilterDirection -> FilterDirection -> Bool
$c<= :: FilterDirection -> FilterDirection -> Bool
< :: FilterDirection -> FilterDirection -> Bool
$c< :: FilterDirection -> FilterDirection -> Bool
compare :: FilterDirection -> FilterDirection -> Ordering
$ccompare :: FilterDirection -> FilterDirection -> Ordering
Ord)

flipFilter :: FilterDirection -> FilterDirection
flipFilter :: FilterDirection -> FilterDirection
flipFilter FilterDirection
FilterRequires = FilterDirection
FilterAllows
flipFilter FilterDirection
FilterAllows   = FilterDirection
FilterRequires

data TypeFilter =
  TypeFilter {
    TypeFilter -> FilterDirection
tfDirection :: FilterDirection,
    -- NOTE: This is GeneralInstance instead of TypeInstanceOrParam so that
    -- param substitution can be done safely.
    TypeFilter -> GeneralInstance
tfType :: GeneralInstance
  } |
  DefinesFilter {
    TypeFilter -> DefinesInstance
dfType :: DefinesInstance
  } |
  ImmutableFilter
  deriving (TypeFilter -> TypeFilter -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: TypeFilter -> TypeFilter -> Bool
$c/= :: TypeFilter -> TypeFilter -> Bool
== :: TypeFilter -> TypeFilter -> Bool
$c== :: TypeFilter -> TypeFilter -> Bool
Eq,Eq TypeFilter
TypeFilter -> TypeFilter -> Bool
TypeFilter -> TypeFilter -> Ordering
TypeFilter -> TypeFilter -> TypeFilter
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: TypeFilter -> TypeFilter -> TypeFilter
$cmin :: TypeFilter -> TypeFilter -> TypeFilter
max :: TypeFilter -> TypeFilter -> TypeFilter
$cmax :: TypeFilter -> TypeFilter -> TypeFilter
>= :: TypeFilter -> TypeFilter -> Bool
$c>= :: TypeFilter -> TypeFilter -> Bool
> :: TypeFilter -> TypeFilter -> Bool
$c> :: TypeFilter -> TypeFilter -> Bool
<= :: TypeFilter -> TypeFilter -> Bool
$c<= :: TypeFilter -> TypeFilter -> Bool
< :: TypeFilter -> TypeFilter -> Bool
$c< :: TypeFilter -> TypeFilter -> Bool
compare :: TypeFilter -> TypeFilter -> Ordering
$ccompare :: TypeFilter -> TypeFilter -> Ordering
Ord)

instance Show TypeFilter where
  show :: TypeFilter -> String
show (TypeFilter FilterDirection
FilterRequires GeneralInstance
t) = String
"requires " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show GeneralInstance
t
  show (TypeFilter FilterDirection
FilterAllows GeneralInstance
t)   = String
"allows "   forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show GeneralInstance
t
  show (DefinesFilter DefinesInstance
t)             = String
"defines "  forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show DefinesInstance
t
  show TypeFilter
ImmutableFilter               = String
"immutable"

isTypeFilter :: TypeFilter -> Bool
isTypeFilter :: TypeFilter -> Bool
isTypeFilter (TypeFilter FilterDirection
_ GeneralInstance
_) = Bool
True
isTypeFilter TypeFilter
_                = Bool
False

isRequiresFilter :: TypeFilter -> Bool
isRequiresFilter :: TypeFilter -> Bool
isRequiresFilter (TypeFilter FilterDirection
FilterRequires GeneralInstance
_) = Bool
True
isRequiresFilter TypeFilter
_                             = Bool
False

isDefinesFilter :: TypeFilter -> Bool
isDefinesFilter :: TypeFilter -> Bool
isDefinesFilter (DefinesFilter DefinesInstance
_) = Bool
True
isDefinesFilter TypeFilter
_                 = Bool
False

isImmutableFilter :: TypeFilter -> Bool
isImmutableFilter :: TypeFilter -> Bool
isImmutableFilter TypeFilter
ImmutableFilter = Bool
True
isImmutableFilter TypeFilter
_               = Bool
False

viewTypeFilter :: ParamName -> TypeFilter -> String
viewTypeFilter :: ParamName -> TypeFilter -> String
viewTypeFilter ParamName
n TypeFilter
f = forall a. Show a => a -> String
show ParamName
n forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show TypeFilter
f

hasInferredParams :: GeneralInstance -> Bool
hasInferredParams :: GeneralInstance -> Bool
hasInferredParams = forall a b.
PreserveMerge a =>
([b] -> b) -> ([b] -> b) -> (T a -> b) -> a -> b
reduceMergeTree forall a (f :: * -> *). (Mergeable a, Foldable f) => f a -> a
mergeAny forall a (f :: * -> *). (Mergeable a, Foldable f) => f a -> a
mergeAny TypeInstanceOrParam -> Bool
checkSingle where
  checkSingle :: TypeInstanceOrParam -> Bool
checkSingle (JustInferredType ParamName
_) = Bool
True
  checkSingle TypeInstanceOrParam
_                    = Bool
False

type InstanceParams = Positional GeneralInstance
type InstanceVariances = Positional Variance
type InstanceFilters = Positional [TypeFilter]

type ParamFilters   = Map.Map ParamName [TypeFilter]
type ParamVariances = Map.Map ParamName Variance
type ParamValues    = Map.Map ParamName GeneralInstance

class TypeResolver r where
  -- Performs parameter substitution for refines.
  trRefines :: CollectErrorsM m =>
    r -> TypeInstance -> CategoryName -> m InstanceParams
  -- Performs parameter substitution for defines.
  trDefines :: CollectErrorsM m =>
    r -> TypeInstance -> CategoryName -> m InstanceParams
  -- Gets the parameter variances for the category.
  trVariance :: CollectErrorsM m =>
    r -> CategoryName -> m InstanceVariances
  -- Gets filters for the assigned parameters.
  trTypeFilters :: CollectErrorsM m =>
    r -> TypeInstance -> m InstanceFilters
  -- Gets filters for the assigned parameters.
  trDefinesFilters :: CollectErrorsM m =>
    r -> DefinesInstance -> m InstanceFilters
  -- Returns True if the type is concrete.
  trConcrete :: CollectErrorsM m =>
    r -> CategoryName -> m Bool
  -- Returns True if the type is immutable.
  trImmutable ::  CollectErrorsM m =>
    r -> CategoryName -> m Bool

data AnyTypeResolver = forall r. TypeResolver r => AnyTypeResolver r

instance TypeResolver AnyTypeResolver where
  trRefines :: forall (m :: * -> *).
CollectErrorsM m =>
AnyTypeResolver -> TypeInstance -> CategoryName -> m InstanceParams
trRefines (AnyTypeResolver r
r) = forall r (m :: * -> *).
(TypeResolver r, CollectErrorsM m) =>
r -> TypeInstance -> CategoryName -> m InstanceParams
trRefines r
r
  trDefines :: forall (m :: * -> *).
CollectErrorsM m =>
AnyTypeResolver -> TypeInstance -> CategoryName -> m InstanceParams
trDefines (AnyTypeResolver r
r) = forall r (m :: * -> *).
(TypeResolver r, CollectErrorsM m) =>
r -> TypeInstance -> CategoryName -> m InstanceParams
trDefines r
r
  trVariance :: forall (m :: * -> *).
CollectErrorsM m =>
AnyTypeResolver -> CategoryName -> m InstanceVariances
trVariance (AnyTypeResolver r
r) = forall r (m :: * -> *).
(TypeResolver r, CollectErrorsM m) =>
r -> CategoryName -> m InstanceVariances
trVariance r
r
  trTypeFilters :: forall (m :: * -> *).
CollectErrorsM m =>
AnyTypeResolver -> TypeInstance -> m InstanceFilters
trTypeFilters (AnyTypeResolver r
r) = forall r (m :: * -> *).
(TypeResolver r, CollectErrorsM m) =>
r -> TypeInstance -> m InstanceFilters
trTypeFilters r
r
  trDefinesFilters :: forall (m :: * -> *).
CollectErrorsM m =>
AnyTypeResolver -> DefinesInstance -> m InstanceFilters
trDefinesFilters (AnyTypeResolver r
r) = forall r (m :: * -> *).
(TypeResolver r, CollectErrorsM m) =>
r -> DefinesInstance -> m InstanceFilters
trDefinesFilters r
r
  trConcrete :: forall (m :: * -> *).
CollectErrorsM m =>
AnyTypeResolver -> CategoryName -> m Bool
trConcrete (AnyTypeResolver r
r) = forall r (m :: * -> *).
(TypeResolver r, CollectErrorsM m) =>
r -> CategoryName -> m Bool
trConcrete r
r
  trImmutable :: forall (m :: * -> *).
CollectErrorsM m =>
AnyTypeResolver -> CategoryName -> m Bool
trImmutable (AnyTypeResolver r
r) = forall r (m :: * -> *).
(TypeResolver r, CollectErrorsM m) =>
r -> CategoryName -> m Bool
trImmutable r
r

filterLookup :: ErrorContextM m =>
  ParamFilters -> ParamName -> m [TypeFilter]
filterLookup :: forall (m :: * -> *).
ErrorContextM m =>
ParamFilters -> ParamName -> m [TypeFilter]
filterLookup ParamFilters
ps ParamName
n = forall {m :: * -> *} {a}. ErrorContextM m => Maybe a -> m a
resolve forall a b. (a -> b) -> a -> b
$ ParamName
n forall k a. Ord k => k -> Map k a -> Maybe a
`Map.lookup` ParamFilters
ps where
  resolve :: Maybe a -> m a
resolve (Just a
x) = forall (m :: * -> *) a. Monad m => a -> m a
return a
x
  resolve Maybe a
_        = forall (m :: * -> *) a. ErrorContextM m => String -> m a
compilerErrorM forall a b. (a -> b) -> a -> b
$ String
"Param " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show ParamName
n forall a. [a] -> [a] -> [a]
++ String
" not found"

getValueForParam :: ErrorContextM m =>
  ParamValues -> ParamName -> m GeneralInstance
getValueForParam :: forall (m :: * -> *).
ErrorContextM m =>
ParamValues -> ParamName -> m GeneralInstance
getValueForParam ParamValues
pa ParamName
n =
  case ParamName
n forall k a. Ord k => k -> Map k a -> Maybe a
`Map.lookup` ParamValues
pa of
       (Just GeneralInstance
x) -> forall (m :: * -> *) a. Monad m => a -> m a
return GeneralInstance
x
       Maybe GeneralInstance
_ -> forall (m :: * -> *) a. ErrorContextM m => String -> m a
compilerErrorM forall a b. (a -> b) -> a -> b
$ String
"Param " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show ParamName
n forall a. [a] -> [a] -> [a]
++ String
" not found"

fixTypeParams :: GeneralInstance -> GeneralInstance
fixTypeParams :: GeneralInstance -> GeneralInstance
fixTypeParams = Bool -> GeneralInstance -> GeneralInstance
setParamsFixed Bool
True

unfixTypeParams :: GeneralInstance -> GeneralInstance
unfixTypeParams :: GeneralInstance -> GeneralInstance
unfixTypeParams = Bool -> GeneralInstance -> GeneralInstance
setParamsFixed Bool
False

setParamsFixed :: Bool -> GeneralInstance -> GeneralInstance
setParamsFixed :: Bool -> GeneralInstance -> GeneralInstance
setParamsFixed Bool
f = forall a b.
(Eq a, Ord a, Eq b, Ord b) =>
(a -> b) -> GeneralType a -> GeneralType b
mapGeneralType TypeInstanceOrParam -> TypeInstanceOrParam
set where
  set :: TypeInstanceOrParam -> TypeInstanceOrParam
set (JustTypeInstance (TypeInstance CategoryName
t InstanceParams
ts)) =
    TypeInstance -> TypeInstanceOrParam
JustTypeInstance forall a b. (a -> b) -> a -> b
$ CategoryName -> InstanceParams -> TypeInstance
TypeInstance CategoryName
t forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Bool -> GeneralInstance -> GeneralInstance
setParamsFixed Bool
f) InstanceParams
ts
  set (JustParamName Bool
_ ParamName
n2) = Bool -> ParamName -> TypeInstanceOrParam
JustParamName Bool
f ParamName
n2
  set TypeInstanceOrParam
t = TypeInstanceOrParam
t

mapTypeGuesses :: MergeTree InferredTypeGuess -> Map.Map ParamName (MergeTree InferredTypeGuess)
mapTypeGuesses :: MergeTree InferredTypeGuess
-> Map ParamName (MergeTree InferredTypeGuess)
mapTypeGuesses = forall a b.
PreserveMerge a =>
([b] -> b) -> ([b] -> b) -> (T a -> b) -> a -> b
reduceMergeTree forall a (f :: * -> *). (Mergeable a, Foldable f) => f a -> a
mergeAny forall a (f :: * -> *). (Mergeable a, Foldable f) => f a -> a
mergeAll InferredTypeGuess -> Map ParamName (MergeTree InferredTypeGuess)
leafToMap where
  leafToMap :: InferredTypeGuess -> Map ParamName (MergeTree InferredTypeGuess)
leafToMap InferredTypeGuess
i = forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(InferredTypeGuess -> ParamName
itgParam InferredTypeGuess
i,forall a. a -> MergeTree a
mergeLeaf InferredTypeGuess
i)]

noInferredTypes :: CollectErrorsM m => m (MergeTree InferredTypeGuess) -> m ()
noInferredTypes :: forall (m :: * -> *).
CollectErrorsM m =>
m (MergeTree InferredTypeGuess) -> m ()
noInferredTypes m (MergeTree InferredTypeGuess)
g = do
  MergeTree InferredTypeGuess
g' <- m (MergeTree InferredTypeGuess)
g
  let gm :: Map ParamName (MergeTree InferredTypeGuess)
gm = MergeTree InferredTypeGuess
-> Map ParamName (MergeTree InferredTypeGuess)
mapTypeGuesses MergeTree InferredTypeGuess
g'
  String
"Type inference is not allowed here" forall (m :: * -> *) a. ErrorContextM m => String -> m a -> m a
!!> forall (m :: * -> *) a b.
CollectErrorsM m =>
(a -> m b) -> [a] -> m ()
mapCompilerM_ forall {a}. MergeTree InferredTypeGuess -> m a
format (forall k a. Map k a -> [a]
Map.elems Map ParamName (MergeTree InferredTypeGuess)
gm) where
    format :: MergeTree InferredTypeGuess -> m a
format = forall (m :: * -> *) a. ErrorContextM m => String -> m a
compilerErrorM forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b.
PreserveMerge a =>
([b] -> b) -> ([b] -> b) -> (T a -> b) -> a -> b
reduceMergeTree [String] -> String
showAny [String] -> String
showAll forall a. Show a => a -> String
show
    showAny :: [String] -> String
showAny [String]
gs = String
"Any of [ " forall a. [a] -> [a] -> [a]
++ forall a. [a] -> [[a]] -> [a]
intercalate String
", " [String]
gs forall a. [a] -> [a] -> [a]
++ String
" ]"
    showAll :: [String] -> String
showAll [String]
gs = String
"All of [ " forall a. [a] -> [a] -> [a]
++ forall a. [a] -> [[a]] -> [a]
intercalate String
", " [String]
gs forall a. [a] -> [a] -> [a]
++ String
" ]"

checkValueAssignment :: (CollectErrorsM m, TypeResolver r) =>
  r -> ParamFilters -> ValueType -> ValueType -> m ()
checkValueAssignment :: forall (m :: * -> *) r.
(CollectErrorsM m, TypeResolver r) =>
r -> ParamFilters -> ValueType -> ValueType -> m ()
checkValueAssignment r
r ParamFilters
f ValueType
t1 ValueType
t2 = forall (m :: * -> *).
CollectErrorsM m =>
m (MergeTree InferredTypeGuess) -> m ()
noInferredTypes forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) r.
(CollectErrorsM m, TypeResolver r) =>
r
-> ParamFilters
-> Variance
-> ValueType
-> ValueType
-> m (MergeTree InferredTypeGuess)
checkValueTypeMatch r
r ParamFilters
f Variance
Covariant ValueType
t1 ValueType
t2

checkValueTypeImmutable :: (CollectErrorsM m, TypeResolver r) => r -> ParamFilters -> ValueType -> m ()
checkValueTypeImmutable :: forall (m :: * -> *) r.
(CollectErrorsM m, TypeResolver r) =>
r -> ParamFilters -> ValueType -> m ()
checkValueTypeImmutable r
r ParamFilters
f (ValueType StorageType
_ GeneralInstance
t) = forall a b.
PreserveMerge a =>
([b] -> b) -> ([b] -> b) -> (T a -> b) -> a -> b
reduceMergeTree forall (f :: * -> *) (m :: * -> *) a.
(Foldable f, CollectErrorsM m) =>
f (m a) -> m ()
collectAllM_ forall (m :: * -> *) (f :: * -> *) a.
(CollectErrorsM m, Foldable f) =>
f (m a) -> m a
collectFirstM forall {m :: * -> *}.
CollectErrorsM m =>
TypeInstanceOrParam -> m ()
leafOp GeneralInstance
t where
  leafOp :: TypeInstanceOrParam -> m ()
leafOp (JustTypeInstance (TypeInstance CategoryName
n InstanceParams
_)) = do
    Bool
immutable <- forall r (m :: * -> *).
(TypeResolver r, CollectErrorsM m) =>
r -> CategoryName -> m Bool
trImmutable r
r CategoryName
n
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool -> Bool
not Bool
immutable) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. ErrorContextM m => String -> m a
compilerErrorM forall a b. (a -> b) -> a -> b
$ String
"Category " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show CategoryName
n forall a. [a] -> [a] -> [a]
++ String
" is not immutable"
  leafOp (JustParamName Bool
_ ParamName
n) = do
    [TypeFilter]
fs <- ParamFilters
f forall (m :: * -> *).
ErrorContextM m =>
ParamFilters -> ParamName -> m [TypeFilter]
`filterLookup` ParamName
n
    forall (m :: * -> *) (f :: * -> *) a.
(CollectErrorsM m, Foldable f) =>
f (m a) -> m a
collectFirstM (forall a b. (a -> b) -> [a] -> [b]
map (forall {m :: * -> *} {a}.
(CollectErrorsM m, Show a) =>
a -> TypeFilter -> m ()
checkFilter ParamName
n) [TypeFilter]
fs) forall (m :: * -> *) a. ErrorContextM m => m a -> String -> m a
<!! String
"No filters imply that " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show ParamName
n forall a. [a] -> [a] -> [a]
++ String
" is immutable"
  leafOp (JustInferredType ParamName
n) = forall (m :: * -> *) a. ErrorContextM m => String -> m a
compilerErrorM forall a b. (a -> b) -> a -> b
$ String
"Inferred type " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show ParamName
n forall a. [a] -> [a] -> [a]
++ String
" is not allowed here"
  checkFilter :: a -> TypeFilter -> m ()
checkFilter a
_ TypeFilter
ImmutableFilter = forall (m :: * -> *) a. Monad m => a -> m a
return ()
  checkFilter a
_ (DefinesFilter (DefinesInstance CategoryName
n2 InstanceParams
_)) = do
    Bool
immutable <- forall r (m :: * -> *).
(TypeResolver r, CollectErrorsM m) =>
r -> CategoryName -> m Bool
trImmutable r
r CategoryName
n2
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool -> Bool
not Bool
immutable) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. ErrorContextM m => String -> m a
compilerErrorM forall a b. (a -> b) -> a -> b
$ String
"Category " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show CategoryName
n2 forall a. [a] -> [a] -> [a]
++ String
" is not immutable"
  checkFilter a
_ (TypeFilter FilterDirection
FilterRequires GeneralInstance
t2) = forall (m :: * -> *) r.
(CollectErrorsM m, TypeResolver r) =>
r -> ParamFilters -> ValueType -> m ()
checkValueTypeImmutable r
r ParamFilters
f (StorageType -> GeneralInstance -> ValueType
ValueType StorageType
RequiredValue GeneralInstance
t2)
  checkFilter a
n TypeFilter
ff =
    forall (m :: * -> *) a. ErrorContextM m => String -> m a
compilerErrorM forall a b. (a -> b) -> a -> b
$ String
"Filter " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show a
n forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show TypeFilter
ff forall a. [a] -> [a] -> [a]
++ String
" does not imply that " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show a
n forall a. [a] -> [a] -> [a]
++ String
" is immutable"

dedupGeneralInstance :: (CollectErrorsM m, TypeResolver r) =>
  r -> ParamFilters -> GeneralInstance -> m GeneralInstance
dedupGeneralInstance :: forall (m :: * -> *) r.
(CollectErrorsM m, TypeResolver r) =>
r -> ParamFilters -> GeneralInstance -> m GeneralInstance
dedupGeneralInstance r
r ParamFilters
f = forall a b.
PreserveMerge a =>
([b] -> b) -> ([b] -> b) -> (T a -> b) -> a -> b
reduceMergeTree [m GeneralInstance] -> m GeneralInstance
dedupAny [m GeneralInstance] -> m GeneralInstance
dedupAll (forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (Eq a, Ord a) => a -> GeneralType a
singleType) where
  dedupAny :: [m GeneralInstance] -> m GeneralInstance
dedupAny = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a (f :: * -> *). (Mergeable a, Foldable f) => f a -> a
mergeAny forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (m :: * -> *) (f :: * -> *) a.
(CollectErrorsM m, Foldable f) =>
f (m a) -> m [a]
collectAllM forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> forall (m :: * -> *) a b.
CollectErrorsM m =>
(a -> a -> m b) -> [a] -> m [a]
mergeObjectsM (forall {m :: * -> *}.
CollectErrorsM m =>
Variance
-> GeneralInstance
-> GeneralInstance
-> m (MergeTree InferredTypeGuess)
checkSingle Variance
Contravariant)) -- [A|B], A<-B => remove B
  dedupAll :: [m GeneralInstance] -> m GeneralInstance
dedupAll = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a (f :: * -> *). (Mergeable a, Foldable f) => f a -> a
mergeAll forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (m :: * -> *) (f :: * -> *) a.
(CollectErrorsM m, Foldable f) =>
f (m a) -> m [a]
collectAllM forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> forall (m :: * -> *) a b.
CollectErrorsM m =>
(a -> a -> m b) -> [a] -> m [a]
mergeObjectsM (forall {m :: * -> *}.
CollectErrorsM m =>
Variance
-> GeneralInstance
-> GeneralInstance
-> m (MergeTree InferredTypeGuess)
checkSingle Variance
Covariant))     -- [A&B], A->B => remove B
  checkSingle :: Variance
-> GeneralInstance
-> GeneralInstance
-> m (MergeTree InferredTypeGuess)
checkSingle Variance
v = forall (m :: * -> *) r.
(CollectErrorsM m, TypeResolver r) =>
r
-> ParamFilters
-> Variance
-> GeneralInstance
-> GeneralInstance
-> m (MergeTree InferredTypeGuess)
checkGeneralMatch r
r ParamFilters
f Variance
v

checkValueTypeMatch :: (CollectErrorsM m, TypeResolver r) =>
  r -> ParamFilters -> Variance -> ValueType -> ValueType -> m (MergeTree InferredTypeGuess)
checkValueTypeMatch :: forall (m :: * -> *) r.
(CollectErrorsM m, TypeResolver r) =>
r
-> ParamFilters
-> Variance
-> ValueType
-> ValueType
-> m (MergeTree InferredTypeGuess)
checkValueTypeMatch r
r ParamFilters
f Variance
v (ValueType StorageType
r1 GeneralInstance
t1) (ValueType StorageType
r2 GeneralInstance
t2) = m (MergeTree InferredTypeGuess)
result where
  result :: m (MergeTree InferredTypeGuess)
result = do
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ Variance
storageDir Variance -> Variance -> Bool
`allowsVariance` Variance
v) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. ErrorContextM m => String -> m a
compilerErrorM String
"Incompatible storage modifiers"
    forall (m :: * -> *) r.
(CollectErrorsM m, TypeResolver r) =>
r
-> ParamFilters
-> Variance
-> GeneralInstance
-> GeneralInstance
-> m (MergeTree InferredTypeGuess)
checkGeneralMatch r
r ParamFilters
f Variance
v GeneralInstance
t1 GeneralInstance
t2
  storageDir :: Variance
storageDir
    | StorageType
r1 forall a. Ord a => a -> a -> Bool
> StorageType
r2   = Variance
Covariant
    | StorageType
r1 forall a. Ord a => a -> a -> Bool
< StorageType
r2   = Variance
Contravariant
    | Bool
otherwise = Variance
Invariant

checkGeneralMatch :: (CollectErrorsM m, TypeResolver r) =>
  r -> ParamFilters -> Variance ->
  GeneralInstance -> GeneralInstance -> m (MergeTree InferredTypeGuess)
checkGeneralMatch :: forall (m :: * -> *) r.
(CollectErrorsM m, TypeResolver r) =>
r
-> ParamFilters
-> Variance
-> GeneralInstance
-> GeneralInstance
-> m (MergeTree InferredTypeGuess)
checkGeneralMatch r
r ParamFilters
f Variance
v GeneralInstance
t1 GeneralInstance
t2 = String
message forall (m :: * -> *) a. ErrorContextM m => String -> m a -> m a
!!> m (MergeTree InferredTypeGuess)
result where
  result :: m (MergeTree InferredTypeGuess)
result = do
    Maybe (TypeInstanceOrParam, TypeInstanceOrParam)
ss <- forall (m :: * -> *) a. CollectErrorsM m => m a -> m (Maybe a)
tryCompilerM m (TypeInstanceOrParam, TypeInstanceOrParam)
bothSingle
    forall (m :: * -> *) (f :: * -> *) a.
(CollectErrorsM m, Foldable f) =>
f (m a) -> m a
collectFirstM [m (MergeTree InferredTypeGuess)
matchInferredRight,forall {m :: * -> *}.
CollectErrorsM m =>
Maybe (TypeInstanceOrParam, TypeInstanceOrParam)
-> m (MergeTree InferredTypeGuess)
getMatcher Maybe (TypeInstanceOrParam, TypeInstanceOrParam)
ss]
  message :: String
message
    | Variance
v forall a. Eq a => a -> a -> Bool
== Variance
Covariant     = String
"Cannot convert " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show GeneralInstance
t1 forall a. [a] -> [a] -> [a]
++ String
" -> "  forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show GeneralInstance
t2
    | Variance
v forall a. Eq a => a -> a -> Bool
== Variance
Contravariant = String
"Cannot convert " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show GeneralInstance
t1 forall a. [a] -> [a] -> [a]
++ String
" <- "  forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show GeneralInstance
t2
    | Bool
otherwise          = String
"Cannot convert " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show GeneralInstance
t1 forall a. [a] -> [a] -> [a]
++ String
" <-> " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show GeneralInstance
t2
  matchNormal :: Variance -> m (MergeTree InferredTypeGuess)
matchNormal Variance
Invariant =
    forall a (m :: * -> *).
(PreserveMerge a, CollectErrorsM m) =>
[m a] -> m a
mergeAllM [Variance -> m (MergeTree InferredTypeGuess)
matchNormal Variance
Contravariant,Variance -> m (MergeTree InferredTypeGuess)
matchNormal Variance
Covariant]
  matchNormal Variance
Contravariant =
    forall a b c.
(PreserveMerge a, PreserveMerge b) =>
([c] -> c) -> ([c] -> c) -> (T a -> T b -> c) -> a -> b -> c
pairMergeTree forall a (m :: * -> *).
(PreserveMerge a, CollectErrorsM m) =>
[m a] -> m a
mergeAnyM forall a (m :: * -> *).
(PreserveMerge a, CollectErrorsM m) =>
[m a] -> m a
mergeAllM (forall (m :: * -> *) r.
(CollectErrorsM m, TypeResolver r) =>
r
-> ParamFilters
-> Variance
-> TypeInstanceOrParam
-> TypeInstanceOrParam
-> m (MergeTree InferredTypeGuess)
checkSingleMatch r
r ParamFilters
f Variance
Contravariant) (forall a. (Eq a, Ord a) => GeneralType a -> GeneralType a
dualGeneralType GeneralInstance
t1) (forall a. (Eq a, Ord a) => GeneralType a -> GeneralType a
dualGeneralType GeneralInstance
t2)
  matchNormal Variance
Covariant =
    forall a b c.
(PreserveMerge a, PreserveMerge b) =>
([c] -> c) -> ([c] -> c) -> (T a -> T b -> c) -> a -> b -> c
pairMergeTree forall a (m :: * -> *).
(PreserveMerge a, CollectErrorsM m) =>
[m a] -> m a
mergeAnyM forall a (m :: * -> *).
(PreserveMerge a, CollectErrorsM m) =>
[m a] -> m a
mergeAllM (forall (m :: * -> *) r.
(CollectErrorsM m, TypeResolver r) =>
r
-> ParamFilters
-> Variance
-> TypeInstanceOrParam
-> TypeInstanceOrParam
-> m (MergeTree InferredTypeGuess)
checkSingleMatch r
r ParamFilters
f Variance
Covariant) GeneralInstance
t1 GeneralInstance
t2
  matchInferredRight :: m (MergeTree InferredTypeGuess)
matchInferredRight = forall a (m :: * -> *).
(PreserveMerge a, CollectErrorsM m) =>
a -> m (T a)
matchOnlyLeaf GeneralInstance
t2 forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall {m :: * -> *}.
CollectErrorsM m =>
TypeInstanceOrParam -> m (MergeTree InferredTypeGuess)
inferFrom
  inferFrom :: TypeInstanceOrParam -> m (MergeTree InferredTypeGuess)
inferFrom (JustInferredType ParamName
p) = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> MergeTree a
mergeLeaf forall a b. (a -> b) -> a -> b
$ ParamName -> GeneralInstance -> Variance -> InferredTypeGuess
InferredTypeGuess ParamName
p GeneralInstance
t1 Variance
v
  inferFrom TypeInstanceOrParam
_ = forall (m :: * -> *) a. CollectErrorsM m => m a
emptyErrorM
  bothSingle :: m (TypeInstanceOrParam, TypeInstanceOrParam)
bothSingle = do
    TypeInstanceOrParam
t1' <- forall a (m :: * -> *).
(PreserveMerge a, CollectErrorsM m) =>
a -> m (T a)
matchOnlyLeaf GeneralInstance
t1
    TypeInstanceOrParam
t2' <- forall a (m :: * -> *).
(PreserveMerge a, CollectErrorsM m) =>
a -> m (T a)
matchOnlyLeaf GeneralInstance
t2
    forall (m :: * -> *) a. Monad m => a -> m a
return (TypeInstanceOrParam
t1',TypeInstanceOrParam
t2')
  getMatcher :: Maybe (TypeInstanceOrParam, TypeInstanceOrParam)
-> m (MergeTree InferredTypeGuess)
getMatcher Maybe (TypeInstanceOrParam, TypeInstanceOrParam)
ss =
    case Maybe (TypeInstanceOrParam, TypeInstanceOrParam)
ss of
         Just (TypeInstanceOrParam
t1',TypeInstanceOrParam
t2') -> forall (m :: * -> *) r.
(CollectErrorsM m, TypeResolver r) =>
r
-> ParamFilters
-> Variance
-> TypeInstanceOrParam
-> TypeInstanceOrParam
-> m (MergeTree InferredTypeGuess)
checkSingleMatch r
r ParamFilters
f Variance
v TypeInstanceOrParam
t1' TypeInstanceOrParam
t2'
         Maybe (TypeInstanceOrParam, TypeInstanceOrParam)
Nothing        -> forall {m :: * -> *}.
CollectErrorsM m =>
Variance -> m (MergeTree InferredTypeGuess)
matchNormal Variance
v

checkSingleMatch :: (CollectErrorsM m, TypeResolver r) =>
  r -> ParamFilters -> Variance ->
  TypeInstanceOrParam -> TypeInstanceOrParam -> m (MergeTree InferredTypeGuess)
checkSingleMatch :: forall (m :: * -> *) r.
(CollectErrorsM m, TypeResolver r) =>
r
-> ParamFilters
-> Variance
-> TypeInstanceOrParam
-> TypeInstanceOrParam
-> m (MergeTree InferredTypeGuess)
checkSingleMatch r
_ ParamFilters
_ Variance
_ (JustInferredType ParamName
p1) TypeInstanceOrParam
_ =
  forall (m :: * -> *) a. ErrorContextM m => String -> m a
compilerErrorM forall a b. (a -> b) -> a -> b
$ String
"Inferred parameter " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show ParamName
p1 forall a. [a] -> [a] -> [a]
++ String
" is not allowed on the left"
checkSingleMatch r
_ ParamFilters
_ Variance
v TypeInstanceOrParam
t1 (JustInferredType ParamName
p2) =
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> MergeTree a
mergeLeaf forall a b. (a -> b) -> a -> b
$ ParamName -> GeneralInstance -> Variance -> InferredTypeGuess
InferredTypeGuess ParamName
p2 (forall a. (Eq a, Ord a) => a -> GeneralType a
singleType TypeInstanceOrParam
t1) Variance
v
checkSingleMatch r
r ParamFilters
f Variance
v (JustTypeInstance TypeInstance
t1) (JustTypeInstance TypeInstance
t2) =
  forall (m :: * -> *) r.
(CollectErrorsM m, TypeResolver r) =>
r
-> ParamFilters
-> Variance
-> TypeInstance
-> TypeInstance
-> m (MergeTree InferredTypeGuess)
checkInstanceToInstance r
r ParamFilters
f Variance
v TypeInstance
t1 TypeInstance
t2
checkSingleMatch r
r ParamFilters
f Variance
v (JustParamName Bool
_ ParamName
p1) (JustTypeInstance TypeInstance
t2) =
  forall (m :: * -> *) r.
(CollectErrorsM m, TypeResolver r) =>
r
-> ParamFilters
-> Variance
-> ParamName
-> TypeInstance
-> m (MergeTree InferredTypeGuess)
checkParamToInstance r
r ParamFilters
f Variance
v ParamName
p1 TypeInstance
t2
checkSingleMatch r
r ParamFilters
f Variance
v (JustTypeInstance TypeInstance
t1) (JustParamName Bool
_ ParamName
p2) =
  forall (m :: * -> *) r.
(CollectErrorsM m, TypeResolver r) =>
r
-> ParamFilters
-> Variance
-> TypeInstance
-> ParamName
-> m (MergeTree InferredTypeGuess)
checkInstanceToParam r
r ParamFilters
f Variance
v TypeInstance
t1 ParamName
p2
checkSingleMatch r
r ParamFilters
f Variance
v (JustParamName Bool
_ ParamName
p1) (JustParamName Bool
_ ParamName
p2) =
  forall (m :: * -> *) r.
(CollectErrorsM m, TypeResolver r) =>
r
-> ParamFilters
-> Variance
-> ParamName
-> ParamName
-> m (MergeTree InferredTypeGuess)
checkParamToParam r
r ParamFilters
f Variance
v ParamName
p1 ParamName
p2

checkInstanceToInstance :: (CollectErrorsM m, TypeResolver r) =>
  r -> ParamFilters -> Variance -> TypeInstance -> TypeInstance -> m (MergeTree InferredTypeGuess)
checkInstanceToInstance :: forall (m :: * -> *) r.
(CollectErrorsM m, TypeResolver r) =>
r
-> ParamFilters
-> Variance
-> TypeInstance
-> TypeInstance
-> m (MergeTree InferredTypeGuess)
checkInstanceToInstance r
r ParamFilters
f Variance
v t1 :: TypeInstance
t1@(TypeInstance CategoryName
n1 InstanceParams
ps1) t2 :: TypeInstance
t2@(TypeInstance CategoryName
n2 InstanceParams
ps2)
  | CategoryName
n1 forall a. Eq a => a -> a -> Bool
== CategoryName
n2 = do
    Positional (GeneralInstance, GeneralInstance)
paired <- forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. [a] -> Positional a
Positional forall a b. (a -> b) -> a -> b
$ forall a b (m :: * -> *) c.
(Show a, Show b, CollectErrorsM m) =>
(a -> b -> m c) -> Positional a -> Positional b -> m [c]
processPairs forall (m :: * -> *) a b. Monad m => a -> b -> m (a, b)
alwaysPair InstanceParams
ps1 InstanceParams
ps2
    InstanceVariances
variance <- forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Variance -> Variance -> Variance
composeVariance Variance
v)) forall a b. (a -> b) -> a -> b
$ forall r (m :: * -> *).
(TypeResolver r, CollectErrorsM m) =>
r -> CategoryName -> m InstanceVariances
trVariance r
r CategoryName
n1
    forall a b c (m :: * -> *).
(Show a, Show b, Mergeable c, CollectErrorsM m) =>
(a -> b -> m c) -> Positional a -> Positional b -> m c
processPairsM (\Variance
v2 (GeneralInstance
p1,GeneralInstance
p2) -> forall (m :: * -> *) r.
(CollectErrorsM m, TypeResolver r) =>
r
-> ParamFilters
-> Variance
-> GeneralInstance
-> GeneralInstance
-> m (MergeTree InferredTypeGuess)
checkGeneralMatch r
r ParamFilters
f Variance
v2 GeneralInstance
p1 GeneralInstance
p2) InstanceVariances
variance Positional (GeneralInstance, GeneralInstance)
paired
  | Variance
v forall a. Eq a => a -> a -> Bool
== Variance
Covariant = do
    InstanceParams
ps1' <- forall r (m :: * -> *).
(TypeResolver r, CollectErrorsM m) =>
r -> TypeInstance -> CategoryName -> m InstanceParams
trRefines r
r TypeInstance
t1 CategoryName
n2
    forall (m :: * -> *) r.
(CollectErrorsM m, TypeResolver r) =>
r
-> ParamFilters
-> Variance
-> TypeInstance
-> TypeInstance
-> m (MergeTree InferredTypeGuess)
checkInstanceToInstance r
r ParamFilters
f Variance
Covariant (CategoryName -> InstanceParams -> TypeInstance
TypeInstance CategoryName
n2 InstanceParams
ps1') TypeInstance
t2
  | Variance
v forall a. Eq a => a -> a -> Bool
== Variance
Contravariant = do
    InstanceParams
ps2' <- forall r (m :: * -> *).
(TypeResolver r, CollectErrorsM m) =>
r -> TypeInstance -> CategoryName -> m InstanceParams
trRefines r
r TypeInstance
t2 CategoryName
n1
    forall (m :: * -> *) r.
(CollectErrorsM m, TypeResolver r) =>
r
-> ParamFilters
-> Variance
-> TypeInstance
-> TypeInstance
-> m (MergeTree InferredTypeGuess)
checkInstanceToInstance r
r ParamFilters
f Variance
Contravariant TypeInstance
t1 (CategoryName -> InstanceParams -> TypeInstance
TypeInstance CategoryName
n1 InstanceParams
ps2')
  | Bool
otherwise = forall (m :: * -> *) a. ErrorContextM m => String -> m a
compilerErrorM forall a b. (a -> b) -> a -> b
$ String
"Category " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show CategoryName
n2 forall a. [a] -> [a] -> [a]
++ String
" is required but got " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show CategoryName
n1

checkParamToInstance :: (CollectErrorsM m, TypeResolver r) =>
  r -> ParamFilters -> Variance -> ParamName -> TypeInstance -> m (MergeTree InferredTypeGuess)
checkParamToInstance :: forall (m :: * -> *) r.
(CollectErrorsM m, TypeResolver r) =>
r
-> ParamFilters
-> Variance
-> ParamName
-> TypeInstance
-> m (MergeTree InferredTypeGuess)
checkParamToInstance r
r ParamFilters
f Variance
Invariant ParamName
n1 TypeInstance
t2 =
  -- Implicit equality, inferred by n1 <-> t2.
  forall a (m :: * -> *).
(PreserveMerge a, CollectErrorsM m) =>
[m a] -> m a
mergeAllM [
      forall (m :: * -> *) r.
(CollectErrorsM m, TypeResolver r) =>
r
-> ParamFilters
-> Variance
-> ParamName
-> TypeInstance
-> m (MergeTree InferredTypeGuess)
checkParamToInstance r
r ParamFilters
f Variance
Covariant     ParamName
n1 TypeInstance
t2,
      forall (m :: * -> *) r.
(CollectErrorsM m, TypeResolver r) =>
r
-> ParamFilters
-> Variance
-> ParamName
-> TypeInstance
-> m (MergeTree InferredTypeGuess)
checkParamToInstance r
r ParamFilters
f Variance
Contravariant ParamName
n1 TypeInstance
t2
    ]
checkParamToInstance r
r ParamFilters
f v :: Variance
v@Variance
Contravariant ParamName
n1 t2 :: TypeInstance
t2@(TypeInstance CategoryName
_ InstanceParams
_) = do
  [TypeFilter]
cs2 <- forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a. (a -> Bool) -> [a] -> [a]
filter TypeFilter -> Bool
isTypeFilter) forall a b. (a -> b) -> a -> b
$ ParamFilters
f forall (m :: * -> *).
ErrorContextM m =>
ParamFilters -> ParamName -> m [TypeFilter]
`filterLookup` ParamName
n1
  forall a (m :: * -> *).
(PreserveMerge a, CollectErrorsM m) =>
[m a] -> m a
mergeAnyM (forall a b. (a -> b) -> [a] -> [b]
map forall {m :: * -> *}.
CollectErrorsM m =>
TypeFilter -> m (MergeTree InferredTypeGuess)
checkConstraintToInstance [TypeFilter]
cs2) forall (m :: * -> *) a. ErrorContextM m => m a -> String -> m a
<!!
    String
"No filters imply " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show TypeInstance
t2 forall a. [a] -> [a] -> [a]
++ String
" <- " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show ParamName
n1 forall a. [a] -> [a] -> [a]
++ String
" in " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Variance
v forall a. [a] -> [a] -> [a]
++ String
" contexts"
  where
    checkConstraintToInstance :: TypeFilter -> m (MergeTree InferredTypeGuess)
checkConstraintToInstance (TypeFilter FilterDirection
FilterAllows GeneralInstance
t) =
      -- F -> x implies T -> x only if T -> F
      forall (m :: * -> *) r.
(CollectErrorsM m, TypeResolver r) =>
r
-> ParamFilters
-> Variance
-> GeneralInstance
-> GeneralInstance
-> m (MergeTree InferredTypeGuess)
checkGeneralMatch r
r ParamFilters
f Variance
v GeneralInstance
t (forall a. (Eq a, Ord a) => a -> GeneralType a
singleType forall a b. (a -> b) -> a -> b
$ TypeInstance -> TypeInstanceOrParam
JustTypeInstance TypeInstance
t2)
    checkConstraintToInstance TypeFilter
f2 =
      -- x -> F cannot imply T -> x
      forall (m :: * -> *) a. ErrorContextM m => String -> m a
compilerErrorM forall a b. (a -> b) -> a -> b
$ String
"Constraint " forall a. [a] -> [a] -> [a]
++ ParamName -> TypeFilter -> String
viewTypeFilter ParamName
n1 TypeFilter
f2 forall a. [a] -> [a] -> [a]
++
                      String
" does not imply " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show TypeInstance
t2 forall a. [a] -> [a] -> [a]
++ String
" <- " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show ParamName
n1
checkParamToInstance r
r ParamFilters
f v :: Variance
v@Variance
Covariant ParamName
n1 t2 :: TypeInstance
t2@(TypeInstance CategoryName
_ InstanceParams
_) = do
  [TypeFilter]
cs1 <- forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a. (a -> Bool) -> [a] -> [a]
filter TypeFilter -> Bool
isTypeFilter) forall a b. (a -> b) -> a -> b
$ ParamFilters
f forall (m :: * -> *).
ErrorContextM m =>
ParamFilters -> ParamName -> m [TypeFilter]
`filterLookup` ParamName
n1
  forall a (m :: * -> *).
(PreserveMerge a, CollectErrorsM m) =>
[m a] -> m a
mergeAnyM (forall a b. (a -> b) -> [a] -> [b]
map forall {m :: * -> *}.
CollectErrorsM m =>
TypeFilter -> m (MergeTree InferredTypeGuess)
checkConstraintToInstance [TypeFilter]
cs1) forall (m :: * -> *) a. ErrorContextM m => m a -> String -> m a
<!!
    String
"No filters imply " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show ParamName
n1 forall a. [a] -> [a] -> [a]
++ String
" -> " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show TypeInstance
t2 forall a. [a] -> [a] -> [a]
++ String
" in " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Variance
v forall a. [a] -> [a] -> [a]
++ String
" contexts"
  where
    checkConstraintToInstance :: TypeFilter -> m (MergeTree InferredTypeGuess)
checkConstraintToInstance (TypeFilter FilterDirection
FilterRequires GeneralInstance
t) =
      -- x -> F implies x -> T only if F -> T
      forall (m :: * -> *) r.
(CollectErrorsM m, TypeResolver r) =>
r
-> ParamFilters
-> Variance
-> GeneralInstance
-> GeneralInstance
-> m (MergeTree InferredTypeGuess)
checkGeneralMatch r
r ParamFilters
f Variance
v GeneralInstance
t (forall a. (Eq a, Ord a) => a -> GeneralType a
singleType forall a b. (a -> b) -> a -> b
$ TypeInstance -> TypeInstanceOrParam
JustTypeInstance TypeInstance
t2)
    checkConstraintToInstance TypeFilter
f2 =
      -- F -> x cannot imply x -> T
      -- DefinesInstance cannot be converted to TypeInstance
      forall (m :: * -> *) a. ErrorContextM m => String -> m a
compilerErrorM forall a b. (a -> b) -> a -> b
$ String
"Constraint " forall a. [a] -> [a] -> [a]
++ ParamName -> TypeFilter -> String
viewTypeFilter ParamName
n1 TypeFilter
f2 forall a. [a] -> [a] -> [a]
++
                      String
" does not imply " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show ParamName
n1 forall a. [a] -> [a] -> [a]
++ String
" -> " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show TypeInstance
t2

checkInstanceToParam :: (CollectErrorsM m, TypeResolver r) =>
  r -> ParamFilters -> Variance -> TypeInstance -> ParamName -> m (MergeTree InferredTypeGuess)
checkInstanceToParam :: forall (m :: * -> *) r.
(CollectErrorsM m, TypeResolver r) =>
r
-> ParamFilters
-> Variance
-> TypeInstance
-> ParamName
-> m (MergeTree InferredTypeGuess)
checkInstanceToParam r
r ParamFilters
f Variance
Invariant TypeInstance
t1 ParamName
n2 =
  -- Implicit equality, inferred by t1 <-> n2.
  forall a (m :: * -> *).
(PreserveMerge a, CollectErrorsM m) =>
[m a] -> m a
mergeAllM [
      forall (m :: * -> *) r.
(CollectErrorsM m, TypeResolver r) =>
r
-> ParamFilters
-> Variance
-> TypeInstance
-> ParamName
-> m (MergeTree InferredTypeGuess)
checkInstanceToParam r
r ParamFilters
f Variance
Covariant     TypeInstance
t1 ParamName
n2,
      forall (m :: * -> *) r.
(CollectErrorsM m, TypeResolver r) =>
r
-> ParamFilters
-> Variance
-> TypeInstance
-> ParamName
-> m (MergeTree InferredTypeGuess)
checkInstanceToParam r
r ParamFilters
f Variance
Contravariant TypeInstance
t1 ParamName
n2
    ]
checkInstanceToParam r
r ParamFilters
f v :: Variance
v@Variance
Contravariant t1 :: TypeInstance
t1@(TypeInstance CategoryName
_ InstanceParams
_) ParamName
n2 = do
  [TypeFilter]
cs1 <- forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a. (a -> Bool) -> [a] -> [a]
filter TypeFilter -> Bool
isTypeFilter) forall a b. (a -> b) -> a -> b
$ ParamFilters
f forall (m :: * -> *).
ErrorContextM m =>
ParamFilters -> ParamName -> m [TypeFilter]
`filterLookup` ParamName
n2
  forall a (m :: * -> *).
(PreserveMerge a, CollectErrorsM m) =>
[m a] -> m a
mergeAnyM (forall a b. (a -> b) -> [a] -> [b]
map forall {m :: * -> *}.
CollectErrorsM m =>
TypeFilter -> m (MergeTree InferredTypeGuess)
checkInstanceToConstraint [TypeFilter]
cs1) forall (m :: * -> *) a. ErrorContextM m => m a -> String -> m a
<!!
    String
"No filters imply " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show ParamName
n2 forall a. [a] -> [a] -> [a]
++ String
" <- " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show TypeInstance
t1 forall a. [a] -> [a] -> [a]
++ String
" in " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Variance
v forall a. [a] -> [a] -> [a]
++ String
" contexts"
  where
    checkInstanceToConstraint :: TypeFilter -> m (MergeTree InferredTypeGuess)
checkInstanceToConstraint (TypeFilter FilterDirection
FilterRequires GeneralInstance
t) =
      -- x -> F implies x -> T only if F -> T
      forall (m :: * -> *) r.
(CollectErrorsM m, TypeResolver r) =>
r
-> ParamFilters
-> Variance
-> GeneralInstance
-> GeneralInstance
-> m (MergeTree InferredTypeGuess)
checkGeneralMatch r
r ParamFilters
f Variance
v (forall a. (Eq a, Ord a) => a -> GeneralType a
singleType forall a b. (a -> b) -> a -> b
$ TypeInstance -> TypeInstanceOrParam
JustTypeInstance TypeInstance
t1) GeneralInstance
t
    checkInstanceToConstraint TypeFilter
f2 =
      -- F -> x cannot imply x -> T
      -- DefinesInstance cannot be converted to TypeInstance
      forall (m :: * -> *) a. ErrorContextM m => String -> m a
compilerErrorM forall a b. (a -> b) -> a -> b
$ String
"Constraint " forall a. [a] -> [a] -> [a]
++ ParamName -> TypeFilter -> String
viewTypeFilter ParamName
n2 TypeFilter
f2 forall a. [a] -> [a] -> [a]
++
                      String
" does not imply " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show ParamName
n2 forall a. [a] -> [a] -> [a]
++ String
" <- " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show TypeInstance
t1
checkInstanceToParam r
r ParamFilters
f v :: Variance
v@Variance
Covariant t1 :: TypeInstance
t1@(TypeInstance CategoryName
_ InstanceParams
_) ParamName
n2 = do
  [TypeFilter]
cs2 <- forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a. (a -> Bool) -> [a] -> [a]
filter TypeFilter -> Bool
isTypeFilter) forall a b. (a -> b) -> a -> b
$ ParamFilters
f forall (m :: * -> *).
ErrorContextM m =>
ParamFilters -> ParamName -> m [TypeFilter]
`filterLookup` ParamName
n2
  forall a (m :: * -> *).
(PreserveMerge a, CollectErrorsM m) =>
[m a] -> m a
mergeAnyM (forall a b. (a -> b) -> [a] -> [b]
map forall {m :: * -> *}.
CollectErrorsM m =>
TypeFilter -> m (MergeTree InferredTypeGuess)
checkInstanceToConstraint [TypeFilter]
cs2) forall (m :: * -> *) a. ErrorContextM m => m a -> String -> m a
<!!
    String
"No filters imply " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show TypeInstance
t1 forall a. [a] -> [a] -> [a]
++ String
" -> " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show ParamName
n2 forall a. [a] -> [a] -> [a]
++ String
" in " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Variance
v forall a. [a] -> [a] -> [a]
++ String
" contexts"
  where
    checkInstanceToConstraint :: TypeFilter -> m (MergeTree InferredTypeGuess)
checkInstanceToConstraint (TypeFilter FilterDirection
FilterAllows GeneralInstance
t) =
      -- F -> x implies T -> x only if T -> F
      forall (m :: * -> *) r.
(CollectErrorsM m, TypeResolver r) =>
r
-> ParamFilters
-> Variance
-> GeneralInstance
-> GeneralInstance
-> m (MergeTree InferredTypeGuess)
checkGeneralMatch r
r ParamFilters
f Variance
v (forall a. (Eq a, Ord a) => a -> GeneralType a
singleType forall a b. (a -> b) -> a -> b
$ TypeInstance -> TypeInstanceOrParam
JustTypeInstance TypeInstance
t1) GeneralInstance
t
    checkInstanceToConstraint TypeFilter
f2 =
      -- x -> F cannot imply T -> x
      forall (m :: * -> *) a. ErrorContextM m => String -> m a
compilerErrorM forall a b. (a -> b) -> a -> b
$ String
"Constraint " forall a. [a] -> [a] -> [a]
++ ParamName -> TypeFilter -> String
viewTypeFilter ParamName
n2 TypeFilter
f2 forall a. [a] -> [a] -> [a]
++
                      String
" does not imply " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show TypeInstance
t1 forall a. [a] -> [a] -> [a]
++ String
" -> " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show ParamName
n2

checkParamToParam :: (CollectErrorsM m, TypeResolver r) =>
  r -> ParamFilters -> Variance -> ParamName -> ParamName -> m (MergeTree InferredTypeGuess)
checkParamToParam :: forall (m :: * -> *) r.
(CollectErrorsM m, TypeResolver r) =>
r
-> ParamFilters
-> Variance
-> ParamName
-> ParamName
-> m (MergeTree InferredTypeGuess)
checkParamToParam r
r ParamFilters
f Variance
Invariant ParamName
n1 ParamName
n2
  | ParamName
n1 forall a. Eq a => a -> a -> Bool
== ParamName
n2 = forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Bounded a => a
maxBound
  | Bool
otherwise =
    -- Implicit equality, inferred by n1 <-> n2.
    forall a (m :: * -> *).
(PreserveMerge a, CollectErrorsM m) =>
[m a] -> m a
mergeAllM [
        forall (m :: * -> *) r.
(CollectErrorsM m, TypeResolver r) =>
r
-> ParamFilters
-> Variance
-> ParamName
-> ParamName
-> m (MergeTree InferredTypeGuess)
checkParamToParam r
r ParamFilters
f Variance
Covariant     ParamName
n1 ParamName
n2,
        forall (m :: * -> *) r.
(CollectErrorsM m, TypeResolver r) =>
r
-> ParamFilters
-> Variance
-> ParamName
-> ParamName
-> m (MergeTree InferredTypeGuess)
checkParamToParam r
r ParamFilters
f Variance
Contravariant ParamName
n1 ParamName
n2
      ]
checkParamToParam r
r ParamFilters
f Variance
v ParamName
n1 ParamName
n2
  | ParamName
n1 forall a. Eq a => a -> a -> Bool
== ParamName
n2 = forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Bounded a => a
maxBound
  | Bool
otherwise = do
    [TypeFilter]
cs1 <- forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a. (a -> Bool) -> [a] -> [a]
filter TypeFilter -> Bool
isTypeFilter) forall a b. (a -> b) -> a -> b
$ ParamFilters
f forall (m :: * -> *).
ErrorContextM m =>
ParamFilters -> ParamName -> m [TypeFilter]
`filterLookup` ParamName
n1
    [TypeFilter]
cs2 <- forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a. (a -> Bool) -> [a] -> [a]
filter TypeFilter -> Bool
isTypeFilter) forall a b. (a -> b) -> a -> b
$ ParamFilters
f forall (m :: * -> *).
ErrorContextM m =>
ParamFilters -> ParamName -> m [TypeFilter]
`filterLookup` ParamName
n2
    let typeFilters :: [(TypeFilter, TypeFilter)]
typeFilters = [(TypeFilter
c1,TypeFilter
c2) | TypeFilter
c1 <- [TypeFilter]
cs1, TypeFilter
c2 <- [TypeFilter]
cs2] forall a. [a] -> [a] -> [a]
++
                      [(TypeFilter
self1,TypeFilter
c2) | TypeFilter
c2 <- [TypeFilter]
cs2] forall a. [a] -> [a] -> [a]
++
                      [(TypeFilter
c1,TypeFilter
self2) | TypeFilter
c1 <- [TypeFilter]
cs1]
    forall a (m :: * -> *).
(PreserveMerge a, CollectErrorsM m) =>
[m a] -> m a
mergeAnyM (forall a b. (a -> b) -> [a] -> [b]
map (\(TypeFilter
c1,TypeFilter
c2) -> forall {m :: * -> *}.
CollectErrorsM m =>
Variance
-> TypeFilter -> TypeFilter -> m (MergeTree InferredTypeGuess)
checkConstraintToConstraint Variance
v TypeFilter
c1 TypeFilter
c2) [(TypeFilter, TypeFilter)]
typeFilters) forall (m :: * -> *) a. ErrorContextM m => m a -> String -> m a
<!!
      String
"No filters imply " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show ParamName
n1 forall a. [a] -> [a] -> [a]
++ String
" -> " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show ParamName
n2
    where
      selfParam1 :: GeneralInstance
selfParam1 = forall a. (Eq a, Ord a) => a -> GeneralType a
singleType forall a b. (a -> b) -> a -> b
$ Bool -> ParamName -> TypeInstanceOrParam
JustParamName Bool
False ParamName
n1
      selfParam2 :: GeneralInstance
selfParam2 = forall a. (Eq a, Ord a) => a -> GeneralType a
singleType forall a b. (a -> b) -> a -> b
$ Bool -> ParamName -> TypeInstanceOrParam
JustParamName Bool
False ParamName
n2
      self1 :: TypeFilter
self1
        | Variance
v forall a. Eq a => a -> a -> Bool
== Variance
Covariant = FilterDirection -> GeneralInstance -> TypeFilter
TypeFilter FilterDirection
FilterRequires GeneralInstance
selfParam1
        | Bool
otherwise      = FilterDirection -> GeneralInstance -> TypeFilter
TypeFilter FilterDirection
FilterAllows   GeneralInstance
selfParam1
      self2 :: TypeFilter
self2
        | Variance
v forall a. Eq a => a -> a -> Bool
== Variance
Covariant = FilterDirection -> GeneralInstance -> TypeFilter
TypeFilter FilterDirection
FilterAllows   GeneralInstance
selfParam2
        | Bool
otherwise      = FilterDirection -> GeneralInstance -> TypeFilter
TypeFilter FilterDirection
FilterRequires GeneralInstance
selfParam2
      checkConstraintToConstraint :: Variance
-> TypeFilter -> TypeFilter -> m (MergeTree InferredTypeGuess)
checkConstraintToConstraint Variance
Covariant (TypeFilter FilterDirection
FilterRequires GeneralInstance
t1) (TypeFilter FilterDirection
FilterAllows GeneralInstance
t2)
        | GeneralInstance
t1 forall a. Eq a => a -> a -> Bool
== GeneralInstance
selfParam1 Bool -> Bool -> Bool
&& GeneralInstance
t2 forall a. Eq a => a -> a -> Bool
== GeneralInstance
selfParam2 =
          forall (m :: * -> *) a. ErrorContextM m => String -> m a
compilerErrorM forall a b. (a -> b) -> a -> b
$ String
"Infinite recursion in " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show ParamName
n1 forall a. [a] -> [a] -> [a]
++ String
" -> " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show ParamName
n2
        -- x -> F1, F2 -> y implies x -> y only if F1 -> F2
        | Bool
otherwise = forall (m :: * -> *) r.
(CollectErrorsM m, TypeResolver r) =>
r
-> ParamFilters
-> Variance
-> GeneralInstance
-> GeneralInstance
-> m (MergeTree InferredTypeGuess)
checkGeneralMatch r
r ParamFilters
f Variance
Covariant GeneralInstance
t1 GeneralInstance
t2
      checkConstraintToConstraint Variance
Covariant TypeFilter
f1 TypeFilter
f2 =
        -- x -> F1, y -> F2 cannot imply x -> y
        -- F1 -> x, F1 -> y cannot imply x -> y
        -- F1 -> x, y -> F2 cannot imply x -> y
        forall (m :: * -> *) a. ErrorContextM m => String -> m a
compilerErrorM forall a b. (a -> b) -> a -> b
$ String
"Constraints " forall a. [a] -> [a] -> [a]
++ ParamName -> TypeFilter -> String
viewTypeFilter ParamName
n1 TypeFilter
f1 forall a. [a] -> [a] -> [a]
++ String
" and " forall a. [a] -> [a] -> [a]
++
                        ParamName -> TypeFilter -> String
viewTypeFilter ParamName
n2 TypeFilter
f2 forall a. [a] -> [a] -> [a]
++ String
" do not imply " forall a. [a] -> [a] -> [a]
++
                        forall a. Show a => a -> String
show ParamName
n1 forall a. [a] -> [a] -> [a]
++ String
" -> " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show ParamName
n2
      checkConstraintToConstraint Variance
Contravariant (TypeFilter FilterDirection
FilterAllows GeneralInstance
t1) (TypeFilter FilterDirection
FilterRequires GeneralInstance
t2)
        | GeneralInstance
t1 forall a. Eq a => a -> a -> Bool
== GeneralInstance
selfParam1 Bool -> Bool -> Bool
&& GeneralInstance
t2 forall a. Eq a => a -> a -> Bool
== GeneralInstance
selfParam2 =
          forall (m :: * -> *) a. ErrorContextM m => String -> m a
compilerErrorM forall a b. (a -> b) -> a -> b
$ String
"Infinite recursion in " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show ParamName
n1 forall a. [a] -> [a] -> [a]
++ String
" <- " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show ParamName
n2
        -- x <- F1, F2 <- y implies x <- y only if F1 <- F2
        | Bool
otherwise = forall (m :: * -> *) r.
(CollectErrorsM m, TypeResolver r) =>
r
-> ParamFilters
-> Variance
-> GeneralInstance
-> GeneralInstance
-> m (MergeTree InferredTypeGuess)
checkGeneralMatch r
r ParamFilters
f Variance
Contravariant GeneralInstance
t1 GeneralInstance
t2
      checkConstraintToConstraint Variance
Contravariant TypeFilter
f1 TypeFilter
f2 =
        -- x <- F1, y <- F2 cannot imply x <- y
        -- F1 <- x, F1 <- y cannot imply x <- y
        -- F1 <- x, y <- F2 cannot imply x <- y
        forall (m :: * -> *) a. ErrorContextM m => String -> m a
compilerErrorM forall a b. (a -> b) -> a -> b
$ String
"Constraints " forall a. [a] -> [a] -> [a]
++ ParamName -> TypeFilter -> String
viewTypeFilter ParamName
n1 TypeFilter
f1 forall a. [a] -> [a] -> [a]
++ String
" and " forall a. [a] -> [a] -> [a]
++
                        ParamName -> TypeFilter -> String
viewTypeFilter ParamName
n2 TypeFilter
f2 forall a. [a] -> [a] -> [a]
++ String
" do not imply " forall a. [a] -> [a] -> [a]
++
                        forall a. Show a => a -> String
show ParamName
n1 forall a. [a] -> [a] -> [a]
++ String
" <- " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show ParamName
n2
      checkConstraintToConstraint Variance
_ TypeFilter
_ TypeFilter
_ = forall a. HasCallStack => a
undefined

validateGeneralInstanceForCall :: (CollectErrorsM m, TypeResolver r) =>
  r -> ParamFilters -> GeneralInstance -> m ()
validateGeneralInstanceForCall :: forall (m :: * -> *) r.
(CollectErrorsM m, TypeResolver r) =>
r -> ParamFilters -> GeneralInstance -> m ()
validateGeneralInstanceForCall r
r ParamFilters
f = forall a b.
PreserveMerge a =>
([b] -> b) -> ([b] -> b) -> (T a -> b) -> a -> b
reduceMergeTree forall (f :: * -> *) (m :: * -> *) a.
(Foldable f, CollectErrorsM m) =>
f (m a) -> m ()
collectAllM_ forall (f :: * -> *) (m :: * -> *) a.
(Foldable f, CollectErrorsM m) =>
f (m a) -> m ()
collectAllM_ forall {m :: * -> *}.
CollectErrorsM m =>
TypeInstanceOrParam -> m ()
validateSingle where
  validateSingle :: TypeInstanceOrParam -> m ()
validateSingle (JustTypeInstance TypeInstance
t) = forall (m :: * -> *) r.
(CollectErrorsM m, TypeResolver r) =>
r -> ParamFilters -> TypeInstance -> m ()
validateTypeInstanceForCall r
r ParamFilters
f TypeInstance
t
  validateSingle (JustParamName Bool
_ ParamName
n) = forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ ParamName
n forall k a. Ord k => k -> Map k a -> Bool
`Map.member` ParamFilters
f) forall a b. (a -> b) -> a -> b
$
      forall (m :: * -> *) a. ErrorContextM m => String -> m a
compilerErrorM forall a b. (a -> b) -> a -> b
$ String
"Param " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show ParamName
n forall a. [a] -> [a] -> [a]
++ String
" not found"
  validateSingle (JustInferredType ParamName
n) = forall (m :: * -> *) a. ErrorContextM m => String -> m a
compilerErrorM forall a b. (a -> b) -> a -> b
$ String
"Inferred param " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show ParamName
n forall a. [a] -> [a] -> [a]
++ String
" is not allowed here"

validateTypeInstanceForCall :: (CollectErrorsM m, TypeResolver r) =>
  r -> ParamFilters -> TypeInstance -> m ()
validateTypeInstanceForCall :: forall (m :: * -> *) r.
(CollectErrorsM m, TypeResolver r) =>
r -> ParamFilters -> TypeInstance -> m ()
validateTypeInstanceForCall r
r ParamFilters
f t :: TypeInstance
t@(TypeInstance CategoryName
_ InstanceParams
ps) = do
  InstanceFilters
fa <- forall r (m :: * -> *).
(TypeResolver r, CollectErrorsM m) =>
r -> TypeInstance -> m InstanceFilters
trTypeFilters r
r TypeInstance
t
  forall a b (m :: * -> *) c.
(Show a, Show b, CollectErrorsM m) =>
(a -> b -> m c) -> Positional a -> Positional b -> m ()
processPairs_ (forall (m :: * -> *) r.
(CollectErrorsM m, TypeResolver r) =>
r -> ParamFilters -> GeneralInstance -> [TypeFilter] -> m ()
validateAssignment r
r ParamFilters
f) InstanceParams
ps InstanceFilters
fa
  forall (m :: * -> *) a b.
CollectErrorsM m =>
(a -> m b) -> [a] -> m ()
mapCompilerM_ (forall (m :: * -> *) r.
(CollectErrorsM m, TypeResolver r) =>
r -> ParamFilters -> GeneralInstance -> m ()
validateGeneralInstanceForCall r
r ParamFilters
f) (forall a. Positional a -> [a]
pValues InstanceParams
ps) forall (m :: * -> *) a. ErrorContextM m => m a -> String -> m a
<?? String
"In " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show TypeInstance
t

validateAssignment :: (CollectErrorsM m, TypeResolver r) =>
  r -> ParamFilters -> GeneralInstance -> [TypeFilter] -> m ()
validateAssignment :: forall (m :: * -> *) r.
(CollectErrorsM m, TypeResolver r) =>
r -> ParamFilters -> GeneralInstance -> [TypeFilter] -> m ()
validateAssignment r
r ParamFilters
f GeneralInstance
t [TypeFilter]
fs = forall (m :: * -> *) a b.
CollectErrorsM m =>
(a -> m b) -> [a] -> m ()
mapCompilerM_ forall {m :: * -> *}. CollectErrorsM m => TypeFilter -> m ()
checkWithMessage [TypeFilter]
fs where
  checkWithMessage :: TypeFilter -> m ()
checkWithMessage TypeFilter
f2 = forall {m :: * -> *}.
CollectErrorsM m =>
GeneralInstance -> TypeFilter -> m ()
checkFilter GeneralInstance
t TypeFilter
f2 forall (m :: * -> *) a. ErrorContextM m => m a -> String -> m a
<?? String
"In verification of filter " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show GeneralInstance
t forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show TypeFilter
f2
  checkFilter :: GeneralInstance -> TypeFilter -> m ()
checkFilter GeneralInstance
t1 (TypeFilter FilterDirection
FilterRequires GeneralInstance
t2) =
    forall (m :: * -> *).
CollectErrorsM m =>
m (MergeTree InferredTypeGuess) -> m ()
noInferredTypes forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) r.
(CollectErrorsM m, TypeResolver r) =>
r
-> ParamFilters
-> Variance
-> GeneralInstance
-> GeneralInstance
-> m (MergeTree InferredTypeGuess)
checkGeneralMatch r
r ParamFilters
f Variance
Covariant GeneralInstance
t1 GeneralInstance
t2
  checkFilter GeneralInstance
t1 (TypeFilter FilterDirection
FilterAllows GeneralInstance
t2) =
    forall (m :: * -> *).
CollectErrorsM m =>
m (MergeTree InferredTypeGuess) -> m ()
noInferredTypes forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) r.
(CollectErrorsM m, TypeResolver r) =>
r
-> ParamFilters
-> Variance
-> GeneralInstance
-> GeneralInstance
-> m (MergeTree InferredTypeGuess)
checkGeneralMatch r
r ParamFilters
f Variance
Contravariant GeneralInstance
t1 GeneralInstance
t2
  checkFilter GeneralInstance
t1 (DefinesFilter DefinesInstance
t2) = do
    TypeInstanceOrParam
t1' <- forall a (m :: * -> *).
(PreserveMerge a, CollectErrorsM m) =>
a -> m (T a)
matchOnlyLeaf GeneralInstance
t1 forall (m :: * -> *) a. ErrorContextM m => m a -> String -> m a
<!! String
"Merged type " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show GeneralInstance
t1 forall a. [a] -> [a] -> [a]
++ String
" cannot satisfy defines constraint " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show DefinesInstance
t2
    forall {m :: * -> *}.
CollectErrorsM m =>
DefinesInstance -> TypeInstanceOrParam -> m ()
checkDefinesFilter DefinesInstance
t2 TypeInstanceOrParam
t1'
  checkFilter GeneralInstance
t1 TypeFilter
ImmutableFilter = forall (m :: * -> *) r.
(CollectErrorsM m, TypeResolver r) =>
r -> ParamFilters -> ValueType -> m ()
checkValueTypeImmutable r
r ParamFilters
f (StorageType -> GeneralInstance -> ValueType
ValueType StorageType
RequiredValue GeneralInstance
t1)
  checkDefinesFilter :: DefinesInstance -> TypeInstanceOrParam -> m ()
checkDefinesFilter f2 :: DefinesInstance
f2@(DefinesInstance CategoryName
n2 InstanceParams
_) (JustTypeInstance TypeInstance
t1) = do
    InstanceParams
ps1' <- forall r (m :: * -> *).
(TypeResolver r, CollectErrorsM m) =>
r -> TypeInstance -> CategoryName -> m InstanceParams
trDefines r
r TypeInstance
t1 CategoryName
n2
    forall (m :: * -> *) r.
(CollectErrorsM m, TypeResolver r) =>
r
-> ParamFilters
-> DefinesInstance
-> DefinesInstance
-> m (MergeTree InferredTypeGuess)
checkDefinesMatch r
r ParamFilters
f (CategoryName -> InstanceParams -> DefinesInstance
DefinesInstance CategoryName
n2 InstanceParams
ps1') DefinesInstance
f2 forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Monad m => a -> m a
return ()
  checkDefinesFilter DefinesInstance
f2 (JustParamName Bool
_ ParamName
n1) = do
      [DefinesInstance]
fs1 <- forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a b. (a -> b) -> [a] -> [b]
map TypeFilter -> DefinesInstance
dfType forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (a -> Bool) -> [a] -> [a]
filter TypeFilter -> Bool
isDefinesFilter) forall a b. (a -> b) -> a -> b
$ ParamFilters
f forall (m :: * -> *).
ErrorContextM m =>
ParamFilters -> ParamName -> m [TypeFilter]
`filterLookup` ParamName
n1
      (forall (f :: * -> *) (m :: * -> *) a.
(Foldable f, CollectErrorsM m) =>
f (m a) -> m ()
collectFirstM_ forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall a b c. (a -> b -> c) -> b -> a -> c
flip (forall (m :: * -> *) r.
(CollectErrorsM m, TypeResolver r) =>
r
-> ParamFilters
-> DefinesInstance
-> DefinesInstance
-> m (MergeTree InferredTypeGuess)
checkDefinesMatch r
r ParamFilters
f) DefinesInstance
f2) [DefinesInstance]
fs1) forall (m :: * -> *) a. ErrorContextM m => m a -> String -> m a
<!!
        String
"No filters imply " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show ParamName
n1 forall a. [a] -> [a] -> [a]
++ String
" defines " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show DefinesInstance
f2
  checkDefinesFilter DefinesInstance
_ (JustInferredType ParamName
n) =
    forall (m :: * -> *) a. ErrorContextM m => String -> m a
compilerErrorM forall a b. (a -> b) -> a -> b
$ String
"Inferred param " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show ParamName
n forall a. [a] -> [a] -> [a]
++ String
" is not allowed here"

checkDefinesMatch :: (CollectErrorsM m, TypeResolver r) =>
  r -> ParamFilters -> DefinesInstance -> DefinesInstance -> m (MergeTree InferredTypeGuess)
checkDefinesMatch :: forall (m :: * -> *) r.
(CollectErrorsM m, TypeResolver r) =>
r
-> ParamFilters
-> DefinesInstance
-> DefinesInstance
-> m (MergeTree InferredTypeGuess)
checkDefinesMatch r
r ParamFilters
f f1 :: DefinesInstance
f1@(DefinesInstance CategoryName
n1 InstanceParams
ps1) f2 :: DefinesInstance
f2@(DefinesInstance CategoryName
n2 InstanceParams
ps2)
  | CategoryName
n1 forall a. Eq a => a -> a -> Bool
== CategoryName
n2 = do
    [(GeneralInstance, GeneralInstance)]
paired <- forall a b (m :: * -> *) c.
(Show a, Show b, CollectErrorsM m) =>
(a -> b -> m c) -> Positional a -> Positional b -> m [c]
processPairs forall (m :: * -> *) a b. Monad m => a -> b -> m (a, b)
alwaysPair InstanceParams
ps1 InstanceParams
ps2
    InstanceVariances
variance <- forall r (m :: * -> *).
(TypeResolver r, CollectErrorsM m) =>
r -> CategoryName -> m InstanceVariances
trVariance r
r CategoryName
n2
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a (f :: * -> *). (Mergeable a, Foldable f) => f a -> a
mergeAll forall a b. (a -> b) -> a -> b
$ forall a b (m :: * -> *) c.
(Show a, Show b, CollectErrorsM m) =>
(a -> b -> m c) -> Positional a -> Positional b -> m [c]
processPairs (\Variance
v2 (GeneralInstance
p1,GeneralInstance
p2) -> forall (m :: * -> *) r.
(CollectErrorsM m, TypeResolver r) =>
r
-> ParamFilters
-> Variance
-> GeneralInstance
-> GeneralInstance
-> m (MergeTree InferredTypeGuess)
checkGeneralMatch r
r ParamFilters
f Variance
v2 GeneralInstance
p1 GeneralInstance
p2) InstanceVariances
variance (forall a. [a] -> Positional a
Positional [(GeneralInstance, GeneralInstance)]
paired)
  | Bool
otherwise = forall (m :: * -> *) a. ErrorContextM m => String -> m a
compilerErrorM forall a b. (a -> b) -> a -> b
$ String
"Constraint " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show DefinesInstance
f1 forall a. [a] -> [a] -> [a]
++ String
" does not imply " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show DefinesInstance
f2

validateGeneralInstance :: (CollectErrorsM m, TypeResolver r) =>
  r -> Set.Set ParamName -> GeneralInstance -> m ()
validateGeneralInstance :: forall (m :: * -> *) r.
(CollectErrorsM m, TypeResolver r) =>
r -> Set ParamName -> GeneralInstance -> m ()
validateGeneralInstance r
r Set ParamName
params = forall a b.
PreserveMerge a =>
([b] -> b) -> ([b] -> b) -> (T a -> b) -> a -> b
reduceMergeTree forall (f :: * -> *) (m :: * -> *) a.
(Foldable f, CollectErrorsM m) =>
f (m a) -> m ()
collectAllM_ forall (f :: * -> *) (m :: * -> *) a.
(Foldable f, CollectErrorsM m) =>
f (m a) -> m ()
collectAllM_ forall {m :: * -> *}.
CollectErrorsM m =>
TypeInstanceOrParam -> m ()
validateSingle where
  validateSingle :: TypeInstanceOrParam -> m ()
validateSingle (JustTypeInstance TypeInstance
t) = forall (m :: * -> *) r.
(CollectErrorsM m, TypeResolver r) =>
r -> Set ParamName -> TypeInstance -> m ()
validateTypeInstance r
r Set ParamName
params TypeInstance
t
  validateSingle (JustParamName Bool
_ ParamName
n) = forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ ParamName
n forall a. Ord a => a -> Set a -> Bool
`Set.member` Set ParamName
params) forall a b. (a -> b) -> a -> b
$
      forall (m :: * -> *) a. ErrorContextM m => String -> m a
compilerErrorM forall a b. (a -> b) -> a -> b
$ String
"Param " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show ParamName
n forall a. [a] -> [a] -> [a]
++ String
" not found"
  validateSingle (JustInferredType ParamName
n) = forall (m :: * -> *) a. ErrorContextM m => String -> m a
compilerErrorM forall a b. (a -> b) -> a -> b
$ String
"Inferred param " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show ParamName
n forall a. [a] -> [a] -> [a]
++ String
" is not allowed here"

validateTypeInstance :: (CollectErrorsM m, TypeResolver r) =>
  r -> Set.Set ParamName -> TypeInstance -> m ()
validateTypeInstance :: forall (m :: * -> *) r.
(CollectErrorsM m, TypeResolver r) =>
r -> Set ParamName -> TypeInstance -> m ()
validateTypeInstance r
r Set ParamName
params t :: TypeInstance
t@(TypeInstance CategoryName
_ InstanceParams
ps) = do
  InstanceFilters
_ <- forall r (m :: * -> *).
(TypeResolver r, CollectErrorsM m) =>
r -> TypeInstance -> m InstanceFilters
trTypeFilters r
r TypeInstance
t  -- This just ensures that t exists.
  forall (m :: * -> *) a b.
CollectErrorsM m =>
(a -> m b) -> [a] -> m ()
mapCompilerM_ (forall (m :: * -> *) r.
(CollectErrorsM m, TypeResolver r) =>
r -> Set ParamName -> GeneralInstance -> m ()
validateGeneralInstance r
r Set ParamName
params) (forall a. Positional a -> [a]
pValues InstanceParams
ps) forall (m :: * -> *) a. ErrorContextM m => m a -> String -> m a
<?? String
"In " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show TypeInstance
t

validateDefinesInstance :: (CollectErrorsM m, TypeResolver r) =>
  r -> Set.Set ParamName -> DefinesInstance -> m ()
validateDefinesInstance :: forall (m :: * -> *) r.
(CollectErrorsM m, TypeResolver r) =>
r -> Set ParamName -> DefinesInstance -> m ()
validateDefinesInstance r
r Set ParamName
params t :: DefinesInstance
t@(DefinesInstance CategoryName
_ InstanceParams
ps) = do
  InstanceFilters
_ <- forall r (m :: * -> *).
(TypeResolver r, CollectErrorsM m) =>
r -> DefinesInstance -> m InstanceFilters
trDefinesFilters r
r DefinesInstance
t  -- This just ensures that t exists.
  forall (m :: * -> *) a b.
CollectErrorsM m =>
(a -> m b) -> [a] -> m ()
mapCompilerM_ (forall (m :: * -> *) r.
(CollectErrorsM m, TypeResolver r) =>
r -> Set ParamName -> GeneralInstance -> m ()
validateGeneralInstance r
r Set ParamName
params) (forall a. Positional a -> [a]
pValues InstanceParams
ps) forall (m :: * -> *) a. ErrorContextM m => m a -> String -> m a
<?? String
"In " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show DefinesInstance
t

validateTypeFilter :: (CollectErrorsM m, TypeResolver r) =>
  r -> Set.Set ParamName -> TypeFilter -> m ()
validateTypeFilter :: forall (m :: * -> *) r.
(CollectErrorsM m, TypeResolver r) =>
r -> Set ParamName -> TypeFilter -> m ()
validateTypeFilter r
r Set ParamName
params (TypeFilter FilterDirection
_ GeneralInstance
t)  = forall (m :: * -> *) r.
(CollectErrorsM m, TypeResolver r) =>
r -> Set ParamName -> GeneralInstance -> m ()
validateGeneralInstance r
r Set ParamName
params GeneralInstance
t
validateTypeFilter r
r Set ParamName
params (DefinesFilter DefinesInstance
t) = forall (m :: * -> *) r.
(CollectErrorsM m, TypeResolver r) =>
r -> Set ParamName -> DefinesInstance -> m ()
validateDefinesInstance r
r Set ParamName
params DefinesInstance
t
validateTypeFilter r
_ Set ParamName
_      TypeFilter
ImmutableFilter   = forall (m :: * -> *) a. Monad m => a -> m a
return ()

validateInstanceVariance :: (CollectErrorsM m, TypeResolver r) =>
  r -> ParamVariances -> Variance -> GeneralInstance -> m ()
validateInstanceVariance :: forall (m :: * -> *) r.
(CollectErrorsM m, TypeResolver r) =>
r -> ParamVariances -> Variance -> GeneralInstance -> m ()
validateInstanceVariance r
r ParamVariances
vm Variance
v = forall a b.
PreserveMerge a =>
([b] -> b) -> ([b] -> b) -> (T a -> b) -> a -> b
reduceMergeTree forall (f :: * -> *) (m :: * -> *) a.
(Foldable f, CollectErrorsM m) =>
f (m a) -> m ()
collectAllM_ forall (f :: * -> *) (m :: * -> *) a.
(Foldable f, CollectErrorsM m) =>
f (m a) -> m ()
collectAllM_ forall {m :: * -> *}.
CollectErrorsM m =>
TypeInstanceOrParam -> m ()
validateSingle where
  vm' :: ParamVariances
vm' = forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert ParamName
ParamSelf Variance
Covariant ParamVariances
vm
  validateSingle :: TypeInstanceOrParam -> m ()
validateSingle (JustTypeInstance (TypeInstance CategoryName
n InstanceParams
ps)) = do
    InstanceVariances
vs <- forall r (m :: * -> *).
(TypeResolver r, CollectErrorsM m) =>
r -> CategoryName -> m InstanceVariances
trVariance r
r CategoryName
n
    [(Variance, GeneralInstance)]
paired <- forall a b (m :: * -> *) c.
(Show a, Show b, CollectErrorsM m) =>
(a -> b -> m c) -> Positional a -> Positional b -> m [c]
processPairs forall (m :: * -> *) a b. Monad m => a -> b -> m (a, b)
alwaysPair InstanceVariances
vs InstanceParams
ps
    forall (m :: * -> *) a b.
CollectErrorsM m =>
(a -> m b) -> [a] -> m ()
mapCompilerM_ (\(Variance
v2,GeneralInstance
p) -> forall (m :: * -> *) r.
(CollectErrorsM m, TypeResolver r) =>
r -> ParamVariances -> Variance -> GeneralInstance -> m ()
validateInstanceVariance r
r ParamVariances
vm' (Variance
v Variance -> Variance -> Variance
`composeVariance` Variance
v2) GeneralInstance
p) [(Variance, GeneralInstance)]
paired
  validateSingle (JustParamName Bool
_ ParamName
n) =
    case ParamName
n forall k a. Ord k => k -> Map k a -> Maybe a
`Map.lookup` ParamVariances
vm' of
        Maybe Variance
Nothing -> forall (m :: * -> *) a. ErrorContextM m => String -> m a
compilerErrorM forall a b. (a -> b) -> a -> b
$ String
"Param " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show ParamName
n forall a. [a] -> [a] -> [a]
++ String
" is undefined"
        (Just Variance
v0) -> forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ Variance
v0 Variance -> Variance -> Bool
`allowsVariance` Variance
v) forall a b. (a -> b) -> a -> b
$
                          forall (m :: * -> *) a. ErrorContextM m => String -> m a
compilerErrorM forall a b. (a -> b) -> a -> b
$ String
"Param " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show ParamName
n forall a. [a] -> [a] -> [a]
++ String
" cannot be " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Variance
v
  validateSingle (JustInferredType ParamName
n) =
    forall (m :: * -> *) a. ErrorContextM m => String -> m a
compilerErrorM forall a b. (a -> b) -> a -> b
$ String
"Inferred param " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show ParamName
n forall a. [a] -> [a] -> [a]
++ String
" is not allowed here"

validateDefinesVariance :: (CollectErrorsM m, TypeResolver r) =>
  r -> ParamVariances -> Variance -> DefinesInstance -> m ()
validateDefinesVariance :: forall (m :: * -> *) r.
(CollectErrorsM m, TypeResolver r) =>
r -> ParamVariances -> Variance -> DefinesInstance -> m ()
validateDefinesVariance r
r ParamVariances
vm Variance
v (DefinesInstance CategoryName
n InstanceParams
ps) = do
  InstanceVariances
vs <- forall r (m :: * -> *).
(TypeResolver r, CollectErrorsM m) =>
r -> CategoryName -> m InstanceVariances
trVariance r
r CategoryName
n
  [(Variance, GeneralInstance)]
paired <- forall a b (m :: * -> *) c.
(Show a, Show b, CollectErrorsM m) =>
(a -> b -> m c) -> Positional a -> Positional b -> m [c]
processPairs forall (m :: * -> *) a b. Monad m => a -> b -> m (a, b)
alwaysPair InstanceVariances
vs InstanceParams
ps
  forall (m :: * -> *) a b.
CollectErrorsM m =>
(a -> m b) -> [a] -> m ()
mapCompilerM_ (\(Variance
v2,GeneralInstance
p) -> forall (m :: * -> *) r.
(CollectErrorsM m, TypeResolver r) =>
r -> ParamVariances -> Variance -> GeneralInstance -> m ()
validateInstanceVariance r
r ParamVariances
vm' (Variance
v Variance -> Variance -> Variance
`composeVariance` Variance
v2) GeneralInstance
p) [(Variance, GeneralInstance)]
paired where
    vm' :: ParamVariances
vm' = forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert ParamName
ParamSelf Variance
Covariant ParamVariances
vm

uncheckedSubValueType :: CollectErrorsM m =>
  (ParamName -> m GeneralInstance) -> ValueType -> m ValueType
uncheckedSubValueType :: forall (m :: * -> *).
CollectErrorsM m =>
(ParamName -> m GeneralInstance) -> ValueType -> m ValueType
uncheckedSubValueType ParamName -> m GeneralInstance
replace (ValueType StorageType
s GeneralInstance
t) = do
  GeneralInstance
t' <- forall (m :: * -> *).
CollectErrorsM m =>
(ParamName -> m GeneralInstance)
-> GeneralInstance -> m GeneralInstance
uncheckedSubInstance ParamName -> m GeneralInstance
replace GeneralInstance
t
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ StorageType -> GeneralInstance -> ValueType
ValueType StorageType
s GeneralInstance
t'

uncheckedSubInstance :: CollectErrorsM m => (ParamName -> m GeneralInstance) ->
  GeneralInstance -> m GeneralInstance
uncheckedSubInstance :: forall (m :: * -> *).
CollectErrorsM m =>
(ParamName -> m GeneralInstance)
-> GeneralInstance -> m GeneralInstance
uncheckedSubInstance ParamName -> m GeneralInstance
replace = forall a b.
PreserveMerge a =>
([b] -> b) -> ([b] -> b) -> (T a -> b) -> a -> b
reduceMergeTree [m GeneralInstance] -> m GeneralInstance
subAny [m GeneralInstance] -> m GeneralInstance
subAll TypeInstanceOrParam -> m GeneralInstance
subSingle where
  -- NOTE: Don't use mergeAnyM because it will fail if the union is empty.
  subAny :: [m GeneralInstance] -> m GeneralInstance
subAny = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a (f :: * -> *). (Mergeable a, Foldable f) => f a -> a
mergeAny forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence
  subAll :: [m GeneralInstance] -> m GeneralInstance
subAll = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a (f :: * -> *). (Mergeable a, Foldable f) => f a -> a
mergeAll forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence
  subSingle :: TypeInstanceOrParam -> m GeneralInstance
subSingle p :: TypeInstanceOrParam
p@(JustParamName Bool
_ ParamName
ParamSelf) = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. (Eq a, Ord a) => a -> GeneralType a
singleType TypeInstanceOrParam
p
  subSingle p :: TypeInstanceOrParam
p@(JustParamName Bool
True ParamName
_)      = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. (Eq a, Ord a) => a -> GeneralType a
singleType TypeInstanceOrParam
p
  subSingle (JustParamName Bool
_ ParamName
n)           = ParamName -> m GeneralInstance
replace ParamName
n
  subSingle (JustInferredType ParamName
n)          = ParamName -> m GeneralInstance
replace ParamName
n
  subSingle (JustTypeInstance TypeInstance
t)          = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a. (Eq a, Ord a) => a -> GeneralType a
singleType forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeInstance -> TypeInstanceOrParam
JustTypeInstance) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
CollectErrorsM m =>
(ParamName -> m GeneralInstance) -> TypeInstance -> m TypeInstance
uncheckedSubSingle ParamName -> m GeneralInstance
replace TypeInstance
t

uncheckedSubSingle :: CollectErrorsM m => (ParamName -> m GeneralInstance) ->
  TypeInstance -> m TypeInstance
uncheckedSubSingle :: forall (m :: * -> *).
CollectErrorsM m =>
(ParamName -> m GeneralInstance) -> TypeInstance -> m TypeInstance
uncheckedSubSingle ParamName -> m GeneralInstance
replace (TypeInstance CategoryName
n (Positional [GeneralInstance]
ts)) = do
  [GeneralInstance]
ts' <- forall (m :: * -> *) a b.
CollectErrorsM m =>
(a -> m b) -> [a] -> m [b]
mapCompilerM (forall (m :: * -> *).
CollectErrorsM m =>
(ParamName -> m GeneralInstance)
-> GeneralInstance -> m GeneralInstance
uncheckedSubInstance ParamName -> m GeneralInstance
replace) [GeneralInstance]
ts
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ CategoryName -> InstanceParams -> TypeInstance
TypeInstance CategoryName
n (forall a. [a] -> Positional a
Positional [GeneralInstance]
ts')

uncheckedSubFilter :: CollectErrorsM m =>
  (ParamName -> m GeneralInstance) -> TypeFilter -> m TypeFilter
uncheckedSubFilter :: forall (m :: * -> *).
CollectErrorsM m =>
(ParamName -> m GeneralInstance) -> TypeFilter -> m TypeFilter
uncheckedSubFilter ParamName -> m GeneralInstance
replace (TypeFilter FilterDirection
d GeneralInstance
t) = do
  GeneralInstance
t' <- forall (m :: * -> *).
CollectErrorsM m =>
(ParamName -> m GeneralInstance)
-> GeneralInstance -> m GeneralInstance
uncheckedSubInstance ParamName -> m GeneralInstance
replace GeneralInstance
t
  forall (m :: * -> *) a. Monad m => a -> m a
return (FilterDirection -> GeneralInstance -> TypeFilter
TypeFilter FilterDirection
d GeneralInstance
t')
uncheckedSubFilter ParamName -> m GeneralInstance
replace (DefinesFilter (DefinesInstance CategoryName
n InstanceParams
ts)) = do
  [GeneralInstance]
ts' <- forall (m :: * -> *) a b.
CollectErrorsM m =>
(a -> m b) -> [a] -> m [b]
mapCompilerM (forall (m :: * -> *).
CollectErrorsM m =>
(ParamName -> m GeneralInstance)
-> GeneralInstance -> m GeneralInstance
uncheckedSubInstance ParamName -> m GeneralInstance
replace) (forall a. Positional a -> [a]
pValues InstanceParams
ts)
  forall (m :: * -> *) a. Monad m => a -> m a
return (DefinesInstance -> TypeFilter
DefinesFilter (CategoryName -> InstanceParams -> DefinesInstance
DefinesInstance CategoryName
n (forall a. [a] -> Positional a
Positional [GeneralInstance]
ts')))
uncheckedSubFilter ParamName -> m GeneralInstance
_ TypeFilter
ImmutableFilter = forall (m :: * -> *) a. Monad m => a -> m a
return TypeFilter
ImmutableFilter

uncheckedSubFilters :: CollectErrorsM m =>
  (ParamName -> m GeneralInstance) -> ParamFilters -> m ParamFilters
uncheckedSubFilters :: forall (m :: * -> *).
CollectErrorsM m =>
(ParamName -> m GeneralInstance) -> ParamFilters -> m ParamFilters
uncheckedSubFilters ParamName -> m GeneralInstance
replace ParamFilters
fa = do
  [(ParamName, [TypeFilter])]
fa' <- forall (m :: * -> *) a b.
CollectErrorsM m =>
(a -> m b) -> [a] -> m [b]
mapCompilerM forall {a}. (a, [TypeFilter]) -> m (a, [TypeFilter])
subParam forall a b. (a -> b) -> a -> b
$ forall k a. Map k a -> [(k, a)]
Map.toList ParamFilters
fa
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(ParamName, [TypeFilter])]
fa'
  where
    subParam :: (a, [TypeFilter]) -> m (a, [TypeFilter])
subParam (a
n,[TypeFilter]
fs) = do
      [TypeFilter]
fs' <- forall (m :: * -> *) a b.
CollectErrorsM m =>
(a -> m b) -> [a] -> m [b]
mapCompilerM (forall (m :: * -> *).
CollectErrorsM m =>
(ParamName -> m GeneralInstance) -> TypeFilter -> m TypeFilter
uncheckedSubFilter ParamName -> m GeneralInstance
replace) [TypeFilter]
fs
      forall (m :: * -> *) a. Monad m => a -> m a
return (a
n,[TypeFilter]
fs')

reverseSelfInstance :: CollectErrorsM m =>
  TypeInstance -> GeneralInstance -> m GeneralInstance
reverseSelfInstance :: forall (m :: * -> *).
CollectErrorsM m =>
TypeInstance -> GeneralInstance -> m GeneralInstance
reverseSelfInstance TypeInstance
self = forall a b.
PreserveMerge a =>
([b] -> b) -> ([b] -> b) -> (T a -> b) -> a -> b
reduceMergeTree [m GeneralInstance] -> m GeneralInstance
subAny [m GeneralInstance] -> m GeneralInstance
subAll forall {m :: * -> *}.
Monad m =>
TypeInstanceOrParam -> m GeneralInstance
subSingle where
  -- NOTE: Don't use mergeAnyM because it will fail if the union is empty.
  subAny :: [m GeneralInstance] -> m GeneralInstance
subAny = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a (f :: * -> *). (Mergeable a, Foldable f) => f a -> a
mergeAny forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence
  subAll :: [m GeneralInstance] -> m GeneralInstance
subAll = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a (f :: * -> *). (Mergeable a, Foldable f) => f a -> a
mergeAll forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence
  -- NOTE: Equality should be fine here, since self should only have param names.
  subSingle :: TypeInstanceOrParam -> m GeneralInstance
subSingle (JustTypeInstance TypeInstance
t) | TypeInstance
t forall a. Eq a => a -> a -> Bool
== TypeInstance
self = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. (Eq a, Ord a) => a -> GeneralType a
singleType forall a b. (a -> b) -> a -> b
$ Bool -> ParamName -> TypeInstanceOrParam
JustParamName Bool
True ParamName
ParamSelf
  subSingle TypeInstanceOrParam
t = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. (Eq a, Ord a) => a -> GeneralType a
singleType TypeInstanceOrParam
t

replaceSelfValueType :: CollectErrorsM m =>
  GeneralInstance -> ValueType -> m ValueType
replaceSelfValueType :: forall (m :: * -> *).
CollectErrorsM m =>
GeneralInstance -> ValueType -> m ValueType
replaceSelfValueType GeneralInstance
self (ValueType StorageType
s GeneralInstance
t) = do
  GeneralInstance
t' <- forall (m :: * -> *).
CollectErrorsM m =>
GeneralInstance -> GeneralInstance -> m GeneralInstance
replaceSelfInstance GeneralInstance
self GeneralInstance
t
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ StorageType -> GeneralInstance -> ValueType
ValueType StorageType
s GeneralInstance
t'

replaceSelfInstance :: CollectErrorsM m =>
  GeneralInstance -> GeneralInstance -> m GeneralInstance
replaceSelfInstance :: forall (m :: * -> *).
CollectErrorsM m =>
GeneralInstance -> GeneralInstance -> m GeneralInstance
replaceSelfInstance GeneralInstance
self = forall a b.
PreserveMerge a =>
([b] -> b) -> ([b] -> b) -> (T a -> b) -> a -> b
reduceMergeTree [m GeneralInstance] -> m GeneralInstance
subAny [m GeneralInstance] -> m GeneralInstance
subAll forall {m :: * -> *}.
CollectErrorsM m =>
TypeInstanceOrParam -> m GeneralInstance
subSingle where
  -- NOTE: Don't use mergeAnyM because it will fail if the union is empty.
  subAny :: [m GeneralInstance] -> m GeneralInstance
subAny = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a (f :: * -> *). (Mergeable a, Foldable f) => f a -> a
mergeAny forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence
  subAll :: [m GeneralInstance] -> m GeneralInstance
subAll = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a (f :: * -> *). (Mergeable a, Foldable f) => f a -> a
mergeAll forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence
  subSingle :: TypeInstanceOrParam -> m GeneralInstance
subSingle (JustParamName Bool
_ ParamName
ParamSelf) = forall (m :: * -> *) a. Monad m => a -> m a
return GeneralInstance
self
  subSingle (JustTypeInstance TypeInstance
t)        = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a. (Eq a, Ord a) => a -> GeneralType a
singleType forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeInstance -> TypeInstanceOrParam
JustTypeInstance) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
CollectErrorsM m =>
GeneralInstance -> TypeInstance -> m TypeInstance
replaceSelfSingle GeneralInstance
self TypeInstance
t
  subSingle TypeInstanceOrParam
t                           = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. (Eq a, Ord a) => a -> GeneralType a
singleType TypeInstanceOrParam
t

replaceSelfSingle :: CollectErrorsM m =>
  GeneralInstance -> TypeInstance -> m TypeInstance
replaceSelfSingle :: forall (m :: * -> *).
CollectErrorsM m =>
GeneralInstance -> TypeInstance -> m TypeInstance
replaceSelfSingle GeneralInstance
self (TypeInstance CategoryName
n (Positional [GeneralInstance]
ts)) = do
  [GeneralInstance]
ts' <- forall (m :: * -> *) a b.
CollectErrorsM m =>
(a -> m b) -> [a] -> m [b]
mapCompilerM (forall (m :: * -> *).
CollectErrorsM m =>
GeneralInstance -> GeneralInstance -> m GeneralInstance
replaceSelfInstance GeneralInstance
self) [GeneralInstance]
ts
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ CategoryName -> InstanceParams -> TypeInstance
TypeInstance CategoryName
n (forall a. [a] -> Positional a
Positional [GeneralInstance]
ts')

replaceSelfFilter :: CollectErrorsM m =>
  GeneralInstance -> TypeFilter -> m TypeFilter
replaceSelfFilter :: forall (m :: * -> *).
CollectErrorsM m =>
GeneralInstance -> TypeFilter -> m TypeFilter
replaceSelfFilter GeneralInstance
self (TypeFilter FilterDirection
d GeneralInstance
t) = do
  GeneralInstance
t' <- forall (m :: * -> *).
CollectErrorsM m =>
GeneralInstance -> GeneralInstance -> m GeneralInstance
replaceSelfInstance GeneralInstance
self GeneralInstance
t
  forall (m :: * -> *) a. Monad m => a -> m a
return (FilterDirection -> GeneralInstance -> TypeFilter
TypeFilter FilterDirection
d GeneralInstance
t')
replaceSelfFilter GeneralInstance
self (DefinesFilter (DefinesInstance CategoryName
n InstanceParams
ts)) = do
  [GeneralInstance]
ts' <- forall (m :: * -> *) a b.
CollectErrorsM m =>
(a -> m b) -> [a] -> m [b]
mapCompilerM (forall (m :: * -> *).
CollectErrorsM m =>
GeneralInstance -> GeneralInstance -> m GeneralInstance
replaceSelfInstance GeneralInstance
self) (forall a. Positional a -> [a]
pValues InstanceParams
ts)
  forall (m :: * -> *) a. Monad m => a -> m a
return (DefinesInstance -> TypeFilter
DefinesFilter (CategoryName -> InstanceParams -> DefinesInstance
DefinesInstance CategoryName
n (forall a. [a] -> Positional a
Positional [GeneralInstance]
ts')))
replaceSelfFilter GeneralInstance
_ TypeFilter
ImmutableFilter = forall (m :: * -> *) a. Monad m => a -> m a
return TypeFilter
ImmutableFilter