{- -----------------------------------------------------------------------------
Copyright 2019-2020 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,
  checkValueTypeMatch,
  filterLookup,
  fixTypeParams,
  flipFilter,
  getValueForParam,
  hasInferredParams,
  isDefinesFilter,
  isRequiresFilter,
  isWeakValue,
  mapTypeGuesses,
  noInferredTypes,
  requiredParam,
  requiredSingleton,
  uncheckedSubFilter,
  uncheckedSubFilters,
  uncheckedSubInstance,
  uncheckedSubSingle,
  uncheckedSubValueType,
  unfixTypeParams,
  validateAssignment,
  validateDefinesInstance,
  validateDefinesVariance,
  validateGeneralInstance,
  validateInstanceVariance,
  validateTypeFilter,
  validateTypeInstance,
) where

import Control.Monad (when)
import Data.List (intercalate)
import qualified Data.Map as Map

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


type GeneralInstance = GeneralType TypeInstanceOrParam

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

data StorageType =
  WeakValue |
  OptionalValue |
  RequiredValue
  deriving (StorageType -> StorageType -> Bool
(StorageType -> StorageType -> Bool)
-> (StorageType -> StorageType -> Bool) -> Eq StorageType
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
Eq StorageType
-> (StorageType -> StorageType -> Ordering)
-> (StorageType -> StorageType -> Bool)
-> (StorageType -> StorageType -> Bool)
-> (StorageType -> StorageType -> Bool)
-> (StorageType -> StorageType -> Bool)
-> (StorageType -> StorageType -> StorageType)
-> (StorageType -> StorageType -> StorageType)
-> Ord 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
$cp1Ord :: Eq StorageType
Ord)

data ValueType =
  ValueType {
    ValueType -> StorageType
vtRequired :: StorageType,
    ValueType -> GeneralInstance
vtType :: GeneralInstance
  }
  deriving (ValueType -> ValueType -> Bool
(ValueType -> ValueType -> Bool)
-> (ValueType -> ValueType -> Bool) -> Eq ValueType
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
Eq ValueType
-> (ValueType -> ValueType -> Ordering)
-> (ValueType -> ValueType -> Bool)
-> (ValueType -> ValueType -> Bool)
-> (ValueType -> ValueType -> Bool)
-> (ValueType -> ValueType -> Bool)
-> (ValueType -> ValueType -> ValueType)
-> (ValueType -> ValueType -> ValueType)
-> Ord 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
$cp1Ord :: Eq ValueType
Ord)

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

isWeakValue :: ValueType -> Bool
isWeakValue :: ValueType -> Bool
isWeakValue = (StorageType -> StorageType -> Bool
forall a. Eq a => a -> a -> Bool
== StorageType
WeakValue) (StorageType -> Bool)
-> (ValueType -> StorageType) -> ValueType -> Bool
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 (GeneralInstance -> ValueType) -> GeneralInstance -> ValueType
forall a b. (a -> b) -> a -> b
$ TypeInstanceOrParam -> GeneralInstance
forall a. (Eq a, Ord a) => a -> GeneralType a
singleType (TypeInstanceOrParam -> GeneralInstance)
-> TypeInstanceOrParam -> GeneralInstance
forall a b. (a -> b) -> a -> b
$ TypeInstance -> TypeInstanceOrParam
JustTypeInstance (TypeInstance -> TypeInstanceOrParam)
-> TypeInstance -> TypeInstanceOrParam
forall a b. (a -> b) -> a -> b
$ CategoryName -> InstanceParams -> TypeInstance
TypeInstance CategoryName
n ([GeneralInstance] -> InstanceParams
forall a. [a] -> Positional a
Positional [])

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

data CategoryName =
  CategoryName {
    CategoryName -> String
tnName :: String
  } |
  BuiltinBool |
  BuiltinChar |
  BuiltinInt |
  BuiltinFloat |
  BuiltinString |
  BuiltinFormatted |
  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
BuiltinInt          = String
"Int"
  show CategoryName
BuiltinFloat        = String
"Float"
  show CategoryName
BuiltinString       = String
"String"
  show CategoryName
BuiltinFormatted    = String
"Formatted"
  show CategoryName
CategoryNone        = String
"(none)"

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

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

newtype ParamName =
  ParamName {
    ParamName -> String
pnName :: String
  }
  deriving (ParamName -> ParamName -> Bool
(ParamName -> ParamName -> Bool)
-> (ParamName -> ParamName -> Bool) -> Eq ParamName
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
Eq ParamName
-> (ParamName -> ParamName -> Ordering)
-> (ParamName -> ParamName -> Bool)
-> (ParamName -> ParamName -> Bool)
-> (ParamName -> ParamName -> Bool)
-> (ParamName -> ParamName -> Bool)
-> (ParamName -> ParamName -> ParamName)
-> (ParamName -> ParamName -> ParamName)
-> Ord 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
$cp1Ord :: Eq ParamName
Ord)

instance Show ParamName where
  show :: ParamName -> String
show (ParamName String
n) = String
n

data TypeInstance =
  TypeInstance {
    TypeInstance -> CategoryName
tiName :: CategoryName,
    TypeInstance -> InstanceParams
tiParams :: InstanceParams
  }
  deriving (TypeInstance -> TypeInstance -> Bool
(TypeInstance -> TypeInstance -> Bool)
-> (TypeInstance -> TypeInstance -> Bool) -> Eq TypeInstance
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
Eq TypeInstance
-> (TypeInstance -> TypeInstance -> Ordering)
-> (TypeInstance -> TypeInstance -> Bool)
-> (TypeInstance -> TypeInstance -> Bool)
-> (TypeInstance -> TypeInstance -> Bool)
-> (TypeInstance -> TypeInstance -> Bool)
-> (TypeInstance -> TypeInstance -> TypeInstance)
-> (TypeInstance -> TypeInstance -> TypeInstance)
-> Ord 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
$cp1Ord :: Eq TypeInstance
Ord)

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

data DefinesInstance =
  DefinesInstance {
    DefinesInstance -> CategoryName
diName :: CategoryName,
    DefinesInstance -> InstanceParams
diParams :: InstanceParams
  }
  deriving (DefinesInstance -> DefinesInstance -> Bool
(DefinesInstance -> DefinesInstance -> Bool)
-> (DefinesInstance -> DefinesInstance -> Bool)
-> Eq DefinesInstance
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
Eq DefinesInstance
-> (DefinesInstance -> DefinesInstance -> Ordering)
-> (DefinesInstance -> DefinesInstance -> Bool)
-> (DefinesInstance -> DefinesInstance -> Bool)
-> (DefinesInstance -> DefinesInstance -> Bool)
-> (DefinesInstance -> DefinesInstance -> Bool)
-> (DefinesInstance -> DefinesInstance -> DefinesInstance)
-> (DefinesInstance -> DefinesInstance -> DefinesInstance)
-> Ord 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
$cp1Ord :: Eq DefinesInstance
Ord)

instance Show DefinesInstance where
  show :: DefinesInstance -> String
show (DefinesInstance CategoryName
n (Positional [])) = CategoryName -> String
forall a. Show a => a -> String
show CategoryName
n
  show (DefinesInstance CategoryName
n (Positional [GeneralInstance]
ts)) =
    CategoryName -> String
forall a. Show a => a -> String
show CategoryName
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"<" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"," ((GeneralInstance -> String) -> [GeneralInstance] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map GeneralInstance -> String
forall a. Show a => a -> String
show [GeneralInstance]
ts) String -> ShowS
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
(InferredTypeGuess -> InferredTypeGuess -> Bool)
-> (InferredTypeGuess -> InferredTypeGuess -> Bool)
-> Eq InferredTypeGuess
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
Eq InferredTypeGuess
-> (InferredTypeGuess -> InferredTypeGuess -> Ordering)
-> (InferredTypeGuess -> InferredTypeGuess -> Bool)
-> (InferredTypeGuess -> InferredTypeGuess -> Bool)
-> (InferredTypeGuess -> InferredTypeGuess -> Bool)
-> (InferredTypeGuess -> InferredTypeGuess -> Bool)
-> (InferredTypeGuess -> InferredTypeGuess -> InferredTypeGuess)
-> (InferredTypeGuess -> InferredTypeGuess -> InferredTypeGuess)
-> Ord 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
$cp1Ord :: Eq InferredTypeGuess
Ord)

instance Show InferredTypeGuess where
  show :: InferredTypeGuess -> String
show (InferredTypeGuess ParamName
n GeneralInstance
g Variance
v) = ParamName -> String
forall a. Show a => a -> String
show ParamName
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ GeneralInstance -> String
forall a. Show a => a -> String
show GeneralInstance
g String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" (" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Variance -> String
forall a. Show a => a -> String
show Variance
v String -> ShowS
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
(TypeInstanceOrParam -> TypeInstanceOrParam -> Bool)
-> (TypeInstanceOrParam -> TypeInstanceOrParam -> Bool)
-> Eq TypeInstanceOrParam
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
Eq TypeInstanceOrParam
-> (TypeInstanceOrParam -> TypeInstanceOrParam -> Ordering)
-> (TypeInstanceOrParam -> TypeInstanceOrParam -> Bool)
-> (TypeInstanceOrParam -> TypeInstanceOrParam -> Bool)
-> (TypeInstanceOrParam -> TypeInstanceOrParam -> Bool)
-> (TypeInstanceOrParam -> TypeInstanceOrParam -> Bool)
-> (TypeInstanceOrParam
    -> TypeInstanceOrParam -> TypeInstanceOrParam)
-> (TypeInstanceOrParam
    -> TypeInstanceOrParam -> TypeInstanceOrParam)
-> Ord 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
$cp1Ord :: Eq TypeInstanceOrParam
Ord)

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

data FilterDirection =
  FilterRequires |
  FilterAllows
  deriving (FilterDirection -> FilterDirection -> Bool
(FilterDirection -> FilterDirection -> Bool)
-> (FilterDirection -> FilterDirection -> Bool)
-> Eq FilterDirection
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
Eq FilterDirection
-> (FilterDirection -> FilterDirection -> Ordering)
-> (FilterDirection -> FilterDirection -> Bool)
-> (FilterDirection -> FilterDirection -> Bool)
-> (FilterDirection -> FilterDirection -> Bool)
-> (FilterDirection -> FilterDirection -> Bool)
-> (FilterDirection -> FilterDirection -> FilterDirection)
-> (FilterDirection -> FilterDirection -> FilterDirection)
-> Ord 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
$cp1Ord :: Eq FilterDirection
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
  }
  deriving (TypeFilter -> TypeFilter -> Bool
(TypeFilter -> TypeFilter -> Bool)
-> (TypeFilter -> TypeFilter -> Bool) -> Eq TypeFilter
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
Eq TypeFilter
-> (TypeFilter -> TypeFilter -> Ordering)
-> (TypeFilter -> TypeFilter -> Bool)
-> (TypeFilter -> TypeFilter -> Bool)
-> (TypeFilter -> TypeFilter -> Bool)
-> (TypeFilter -> TypeFilter -> Bool)
-> (TypeFilter -> TypeFilter -> TypeFilter)
-> (TypeFilter -> TypeFilter -> TypeFilter)
-> Ord 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
$cp1Ord :: Eq TypeFilter
Ord)

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

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

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

hasInferredParams :: GeneralInstance -> Bool
hasInferredParams :: GeneralInstance -> Bool
hasInferredParams = ([Bool] -> Bool)
-> ([Bool] -> Bool)
-> (T GeneralInstance -> Bool)
-> GeneralInstance
-> Bool
forall a b.
PreserveMerge a =>
([b] -> b) -> ([b] -> b) -> (T a -> b) -> a -> b
reduceMergeTree [Bool] -> Bool
forall a (f :: * -> *). (Mergeable a, Foldable f) => f a -> a
mergeAny [Bool] -> Bool
forall a (f :: * -> *). (Mergeable a, Foldable f) => f a -> a
mergeAny T GeneralInstance -> Bool
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 :: CompileErrorM m =>
    r -> TypeInstance -> CategoryName -> m InstanceParams
  -- Performs parameter substitution for defines.
  trDefines :: CompileErrorM m =>
    r -> TypeInstance -> CategoryName -> m InstanceParams
  -- Get the parameter variances for the category.
  trVariance :: CompileErrorM m =>
    r -> CategoryName -> m InstanceVariances
  -- Gets filters for the assigned parameters.
  trTypeFilters :: CompileErrorM m =>
    r -> TypeInstance -> m InstanceFilters
  -- Gets filters for the assigned parameters.
  trDefinesFilters :: CompileErrorM m =>
    r -> DefinesInstance -> m InstanceFilters
  -- Returns True if the type is concrete.
  trConcrete :: CompileErrorM m =>
    r -> CategoryName -> m Bool

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

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

filterLookup :: CompileErrorM m =>
  ParamFilters -> ParamName -> m [TypeFilter]
filterLookup :: ParamFilters -> ParamName -> m [TypeFilter]
filterLookup ParamFilters
ps ParamName
n = Maybe [TypeFilter] -> m [TypeFilter]
forall (m :: * -> *) a. CompileErrorM m => Maybe a -> m a
resolve (Maybe [TypeFilter] -> m [TypeFilter])
-> Maybe [TypeFilter] -> m [TypeFilter]
forall a b. (a -> b) -> a -> b
$ ParamName
n ParamName -> ParamFilters -> Maybe [TypeFilter]
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) = a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return a
x
  resolve Maybe a
_        = String -> m a
forall (m :: * -> *) a. CompileErrorM m => String -> m a
compileErrorM (String -> m a) -> String -> m a
forall a b. (a -> b) -> a -> b
$ String
"Param " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ParamName -> String
forall a. Show a => a -> String
show ParamName
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" not found"

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

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 = (TypeInstanceOrParam -> TypeInstanceOrParam)
-> GeneralInstance -> GeneralInstance
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 (TypeInstance -> TypeInstanceOrParam)
-> TypeInstance -> TypeInstanceOrParam
forall a b. (a -> b) -> a -> b
$ CategoryName -> InstanceParams -> TypeInstance
TypeInstance CategoryName
t (InstanceParams -> TypeInstance) -> InstanceParams -> TypeInstance
forall a b. (a -> b) -> a -> b
$ (GeneralInstance -> GeneralInstance)
-> InstanceParams -> InstanceParams
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 = ([Map ParamName (MergeTree InferredTypeGuess)]
 -> Map ParamName (MergeTree InferredTypeGuess))
-> ([Map ParamName (MergeTree InferredTypeGuess)]
    -> Map ParamName (MergeTree InferredTypeGuess))
-> (T (MergeTree InferredTypeGuess)
    -> Map ParamName (MergeTree InferredTypeGuess))
-> MergeTree InferredTypeGuess
-> Map ParamName (MergeTree InferredTypeGuess)
forall a b.
PreserveMerge a =>
([b] -> b) -> ([b] -> b) -> (T a -> b) -> a -> b
reduceMergeTree [Map ParamName (MergeTree InferredTypeGuess)]
-> Map ParamName (MergeTree InferredTypeGuess)
forall a (f :: * -> *). (Mergeable a, Foldable f) => f a -> a
mergeAny [Map ParamName (MergeTree InferredTypeGuess)]
-> Map ParamName (MergeTree InferredTypeGuess)
forall a (f :: * -> *). (Mergeable a, Foldable f) => f a -> a
mergeAll T (MergeTree InferredTypeGuess)
-> Map ParamName (MergeTree InferredTypeGuess)
InferredTypeGuess -> Map ParamName (MergeTree InferredTypeGuess)
leafToMap where
  leafToMap :: InferredTypeGuess -> Map ParamName (MergeTree InferredTypeGuess)
leafToMap InferredTypeGuess
i = [(ParamName, MergeTree InferredTypeGuess)]
-> Map ParamName (MergeTree InferredTypeGuess)
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(InferredTypeGuess -> ParamName
itgParam InferredTypeGuess
i,InferredTypeGuess -> MergeTree InferredTypeGuess
forall a. a -> MergeTree a
mergeLeaf InferredTypeGuess
i)]

noInferredTypes :: CompileErrorM m => m (MergeTree InferredTypeGuess) -> m ()
noInferredTypes :: 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" String -> m () -> m ()
forall (m :: * -> *) a. CompileErrorM m => String -> m a -> m a
!!> ((MergeTree InferredTypeGuess -> m Any)
-> [MergeTree InferredTypeGuess] -> m ()
forall (m :: * -> *) a b.
CompileErrorM m =>
(a -> m b) -> [a] -> m ()
mapErrorsM_ MergeTree InferredTypeGuess -> m Any
forall a. MergeTree InferredTypeGuess -> m a
format ([MergeTree InferredTypeGuess] -> m ())
-> [MergeTree InferredTypeGuess] -> m ()
forall a b. (a -> b) -> a -> b
$ Map ParamName (MergeTree InferredTypeGuess)
-> [MergeTree InferredTypeGuess]
forall k a. Map k a -> [a]
Map.elems Map ParamName (MergeTree InferredTypeGuess)
gm) where
    format :: MergeTree InferredTypeGuess -> m a
format = String -> m a
forall (m :: * -> *) a. CompileErrorM m => String -> m a
compileErrorM (String -> m a)
-> (MergeTree InferredTypeGuess -> String)
-> MergeTree InferredTypeGuess
-> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([String] -> String)
-> ([String] -> String)
-> (T (MergeTree InferredTypeGuess) -> String)
-> MergeTree InferredTypeGuess
-> String
forall a b.
PreserveMerge a =>
([b] -> b) -> ([b] -> b) -> (T a -> b) -> a -> b
reduceMergeTree [String] -> String
showAny [String] -> String
showAll T (MergeTree InferredTypeGuess) -> String
forall a. Show a => a -> String
show
    showAny :: [String] -> String
showAny [String]
gs = String
"Any of [ " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
", " [String]
gs String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" ]"
    showAll :: [String] -> String
showAll [String]
gs = String
"All of [ " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
", " [String]
gs String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" ]"

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

checkValueTypeMatch :: (CompileErrorM m, TypeResolver r) =>
  r -> ParamFilters -> Variance -> ValueType -> ValueType -> m (MergeTree InferredTypeGuess)
checkValueTypeMatch :: r
-> ParamFilters
-> Variance
-> ValueType
-> ValueType
-> m (MergeTree InferredTypeGuess)
checkValueTypeMatch r
r ParamFilters
f Variance
v ts1 :: ValueType
ts1@(ValueType StorageType
r1 GeneralInstance
t1) ts2 :: ValueType
ts2@(ValueType StorageType
r2 GeneralInstance
t2) = m (MergeTree InferredTypeGuess)
result m (MergeTree InferredTypeGuess)
-> String -> m (MergeTree InferredTypeGuess)
forall (m :: * -> *) a. CompileErrorM m => m a -> String -> m a
<!! String
message where
  message :: String
message
    | Variance
v Variance -> Variance -> Bool
forall a. Eq a => a -> a -> Bool
== Variance
Covariant     = String
"Cannot convert " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ValueType -> String
forall a. Show a => a -> String
show ValueType
ts1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" -> "  String -> ShowS
forall a. [a] -> [a] -> [a]
++ ValueType -> String
forall a. Show a => a -> String
show ValueType
ts2
    | Variance
v Variance -> Variance -> Bool
forall a. Eq a => a -> a -> Bool
== Variance
Contravariant = String
"Cannot convert " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ValueType -> String
forall a. Show a => a -> String
show ValueType
ts1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" <- "  String -> ShowS
forall a. [a] -> [a] -> [a]
++ ValueType -> String
forall a. Show a => a -> String
show ValueType
ts2
    | Bool
otherwise          = String
"Cannot convert " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ValueType -> String
forall a. Show a => a -> String
show ValueType
ts1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" <-> " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ValueType -> String
forall a. Show a => a -> String
show ValueType
ts2
  storageDir :: Variance
storageDir
    | StorageType
r1 StorageType -> StorageType -> Bool
forall a. Ord a => a -> a -> Bool
> StorageType
r2   = Variance
Covariant
    | StorageType
r1 StorageType -> StorageType -> Bool
forall a. Ord a => a -> a -> Bool
< StorageType
r2   = Variance
Contravariant
    | Bool
otherwise = Variance
Invariant
  result :: m (MergeTree InferredTypeGuess)
result = do
    Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Variance
storageDir Variance -> Variance -> Bool
`allowsVariance` Variance
v) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ String -> m ()
forall (m :: * -> *) a. CompileErrorM m => String -> m a
compileErrorM String
"Incompatible storage modifiers"
    r
-> ParamFilters
-> Variance
-> GeneralInstance
-> GeneralInstance
-> m (MergeTree InferredTypeGuess)
forall (m :: * -> *) r.
(CompileErrorM m, TypeResolver r) =>
r
-> ParamFilters
-> Variance
-> GeneralInstance
-> GeneralInstance
-> m (MergeTree InferredTypeGuess)
checkGeneralMatch r
r ParamFilters
f Variance
v GeneralInstance
t1 GeneralInstance
t2

checkGeneralMatch :: (CompileErrorM m, TypeResolver r) =>
  r -> ParamFilters -> Variance ->
  GeneralInstance -> GeneralInstance -> m (MergeTree InferredTypeGuess)
checkGeneralMatch :: r
-> ParamFilters
-> Variance
-> GeneralInstance
-> GeneralInstance
-> m (MergeTree InferredTypeGuess)
checkGeneralMatch r
r ParamFilters
f Variance
v GeneralInstance
t1 GeneralInstance
t2 = do
  Maybe (TypeInstanceOrParam, TypeInstanceOrParam)
ss <- [m (Maybe (TypeInstanceOrParam, TypeInstanceOrParam))]
-> m (Maybe (TypeInstanceOrParam, TypeInstanceOrParam))
forall (m :: * -> *) (f :: * -> *) a.
(CompileErrorM m, Foldable f) =>
f (m a) -> m a
collectFirstM [((TypeInstanceOrParam, TypeInstanceOrParam)
 -> Maybe (TypeInstanceOrParam, TypeInstanceOrParam))
-> m (TypeInstanceOrParam, TypeInstanceOrParam)
-> m (Maybe (TypeInstanceOrParam, TypeInstanceOrParam))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (TypeInstanceOrParam, TypeInstanceOrParam)
-> Maybe (TypeInstanceOrParam, TypeInstanceOrParam)
forall a. a -> Maybe a
Just m (TypeInstanceOrParam, TypeInstanceOrParam)
bothSingle,Maybe (TypeInstanceOrParam, TypeInstanceOrParam)
-> m (Maybe (TypeInstanceOrParam, TypeInstanceOrParam))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (TypeInstanceOrParam, TypeInstanceOrParam)
forall a. Maybe a
Nothing]
  [m (MergeTree InferredTypeGuess)]
-> m (MergeTree InferredTypeGuess)
forall (m :: * -> *) (f :: * -> *) a.
(CompileErrorM m, Foldable f) =>
f (m a) -> m a
collectFirstM [m (MergeTree InferredTypeGuess)
matchInferredRight,Maybe (TypeInstanceOrParam, TypeInstanceOrParam)
-> m (MergeTree InferredTypeGuess)
forall (m :: * -> *).
CompileErrorM m =>
Maybe (TypeInstanceOrParam, TypeInstanceOrParam)
-> m (MergeTree InferredTypeGuess)
getMatcher Maybe (TypeInstanceOrParam, TypeInstanceOrParam)
ss] where
  matchNormal :: Variance -> m (MergeTree InferredTypeGuess)
matchNormal Variance
Invariant =
    [m (MergeTree InferredTypeGuess)]
-> m (MergeTree InferredTypeGuess)
forall a (m :: * -> *).
(PreserveMerge a, CompileErrorM m) =>
[m a] -> m a
mergeAllM [Variance -> m (MergeTree InferredTypeGuess)
matchNormal Variance
Contravariant,Variance -> m (MergeTree InferredTypeGuess)
matchNormal Variance
Covariant]
  matchNormal Variance
Contravariant =
    ([m (MergeTree InferredTypeGuess)]
 -> m (MergeTree InferredTypeGuess))
-> ([m (MergeTree InferredTypeGuess)]
    -> m (MergeTree InferredTypeGuess))
-> (T GeneralInstance
    -> T GeneralInstance -> m (MergeTree InferredTypeGuess))
-> GeneralInstance
-> GeneralInstance
-> m (MergeTree InferredTypeGuess)
forall a b c.
(PreserveMerge a, PreserveMerge b) =>
([c] -> c) -> ([c] -> c) -> (T a -> T b -> c) -> a -> b -> c
pairMergeTree [m (MergeTree InferredTypeGuess)]
-> m (MergeTree InferredTypeGuess)
forall a (m :: * -> *).
(PreserveMerge a, CompileErrorM m) =>
[m a] -> m a
mergeAnyM [m (MergeTree InferredTypeGuess)]
-> m (MergeTree InferredTypeGuess)
forall a (m :: * -> *).
(PreserveMerge a, CompileErrorM m) =>
[m a] -> m a
mergeAllM (r
-> ParamFilters
-> Variance
-> TypeInstanceOrParam
-> TypeInstanceOrParam
-> m (MergeTree InferredTypeGuess)
forall (m :: * -> *) r.
(CompileErrorM m, TypeResolver r) =>
r
-> ParamFilters
-> Variance
-> TypeInstanceOrParam
-> TypeInstanceOrParam
-> m (MergeTree InferredTypeGuess)
checkSingleMatch r
r ParamFilters
f Variance
Contravariant) (GeneralInstance -> GeneralInstance
forall a. (Eq a, Ord a) => GeneralType a -> GeneralType a
dualGeneralType GeneralInstance
t1) (GeneralInstance -> GeneralInstance
forall a. (Eq a, Ord a) => GeneralType a -> GeneralType a
dualGeneralType GeneralInstance
t2)
  matchNormal Variance
Covariant =
    ([m (MergeTree InferredTypeGuess)]
 -> m (MergeTree InferredTypeGuess))
-> ([m (MergeTree InferredTypeGuess)]
    -> m (MergeTree InferredTypeGuess))
-> (T GeneralInstance
    -> T GeneralInstance -> m (MergeTree InferredTypeGuess))
-> GeneralInstance
-> GeneralInstance
-> m (MergeTree InferredTypeGuess)
forall a b c.
(PreserveMerge a, PreserveMerge b) =>
([c] -> c) -> ([c] -> c) -> (T a -> T b -> c) -> a -> b -> c
pairMergeTree [m (MergeTree InferredTypeGuess)]
-> m (MergeTree InferredTypeGuess)
forall a (m :: * -> *).
(PreserveMerge a, CompileErrorM m) =>
[m a] -> m a
mergeAnyM [m (MergeTree InferredTypeGuess)]
-> m (MergeTree InferredTypeGuess)
forall a (m :: * -> *).
(PreserveMerge a, CompileErrorM m) =>
[m a] -> m a
mergeAllM (r
-> ParamFilters
-> Variance
-> TypeInstanceOrParam
-> TypeInstanceOrParam
-> m (MergeTree InferredTypeGuess)
forall (m :: * -> *) r.
(CompileErrorM 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 = GeneralInstance -> m (T GeneralInstance)
forall a (m :: * -> *).
(PreserveMerge a, CompileErrorM m) =>
a -> m (T a)
matchOnlyLeaf GeneralInstance
t2 m TypeInstanceOrParam
-> (TypeInstanceOrParam -> m (MergeTree InferredTypeGuess))
-> m (MergeTree InferredTypeGuess)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= TypeInstanceOrParam -> m (MergeTree InferredTypeGuess)
forall (m :: * -> *).
CompileErrorM m =>
TypeInstanceOrParam -> m (MergeTree InferredTypeGuess)
inferFrom
  inferFrom :: TypeInstanceOrParam -> m (MergeTree InferredTypeGuess)
inferFrom (JustInferredType ParamName
p) = MergeTree InferredTypeGuess -> m (MergeTree InferredTypeGuess)
forall (m :: * -> *) a. Monad m => a -> m a
return (MergeTree InferredTypeGuess -> m (MergeTree InferredTypeGuess))
-> MergeTree InferredTypeGuess -> m (MergeTree InferredTypeGuess)
forall a b. (a -> b) -> a -> b
$ InferredTypeGuess -> MergeTree InferredTypeGuess
forall a. a -> MergeTree a
mergeLeaf (InferredTypeGuess -> MergeTree InferredTypeGuess)
-> InferredTypeGuess -> MergeTree InferredTypeGuess
forall a b. (a -> b) -> a -> b
$ ParamName -> GeneralInstance -> Variance -> InferredTypeGuess
InferredTypeGuess ParamName
p GeneralInstance
t1 Variance
v
  inferFrom TypeInstanceOrParam
_ = String -> m (MergeTree InferredTypeGuess)
forall (m :: * -> *) a. CompileErrorM m => String -> m a
compileErrorM String
""
  bothSingle :: m (TypeInstanceOrParam, TypeInstanceOrParam)
bothSingle = do
    TypeInstanceOrParam
t1' <- GeneralInstance -> m (T GeneralInstance)
forall a (m :: * -> *).
(PreserveMerge a, CompileErrorM m) =>
a -> m (T a)
matchOnlyLeaf GeneralInstance
t1
    TypeInstanceOrParam
t2' <- GeneralInstance -> m (T GeneralInstance)
forall a (m :: * -> *).
(PreserveMerge a, CompileErrorM m) =>
a -> m (T a)
matchOnlyLeaf GeneralInstance
t2
    (TypeInstanceOrParam, TypeInstanceOrParam)
-> m (TypeInstanceOrParam, TypeInstanceOrParam)
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') -> r
-> ParamFilters
-> Variance
-> TypeInstanceOrParam
-> TypeInstanceOrParam
-> m (MergeTree InferredTypeGuess)
forall (m :: * -> *) r.
(CompileErrorM 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        -> Variance -> m (MergeTree InferredTypeGuess)
forall (m :: * -> *).
CompileErrorM m =>
Variance -> m (MergeTree InferredTypeGuess)
matchNormal Variance
v

checkSingleMatch :: (CompileErrorM m, TypeResolver r) =>
  r -> ParamFilters -> Variance ->
  TypeInstanceOrParam -> TypeInstanceOrParam -> m (MergeTree InferredTypeGuess)
checkSingleMatch :: r
-> ParamFilters
-> Variance
-> TypeInstanceOrParam
-> TypeInstanceOrParam
-> m (MergeTree InferredTypeGuess)
checkSingleMatch r
_ ParamFilters
_ Variance
_ (JustInferredType ParamName
p1) TypeInstanceOrParam
_ =
  String -> m (MergeTree InferredTypeGuess)
forall (m :: * -> *) a. CompileErrorM m => String -> m a
compileErrorM (String -> m (MergeTree InferredTypeGuess))
-> String -> m (MergeTree InferredTypeGuess)
forall a b. (a -> b) -> a -> b
$ String
"Inferred parameter " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ParamName -> String
forall a. Show a => a -> String
show ParamName
p1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" is not allowed on the left"
checkSingleMatch r
_ ParamFilters
_ Variance
v TypeInstanceOrParam
t1 (JustInferredType ParamName
p2) =
  MergeTree InferredTypeGuess -> m (MergeTree InferredTypeGuess)
forall (m :: * -> *) a. Monad m => a -> m a
return (MergeTree InferredTypeGuess -> m (MergeTree InferredTypeGuess))
-> MergeTree InferredTypeGuess -> m (MergeTree InferredTypeGuess)
forall a b. (a -> b) -> a -> b
$ InferredTypeGuess -> MergeTree InferredTypeGuess
forall a. a -> MergeTree a
mergeLeaf (InferredTypeGuess -> MergeTree InferredTypeGuess)
-> InferredTypeGuess -> MergeTree InferredTypeGuess
forall a b. (a -> b) -> a -> b
$ ParamName -> GeneralInstance -> Variance -> InferredTypeGuess
InferredTypeGuess ParamName
p2 (TypeInstanceOrParam -> GeneralInstance
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) =
  r
-> ParamFilters
-> Variance
-> TypeInstance
-> TypeInstance
-> m (MergeTree InferredTypeGuess)
forall (m :: * -> *) r.
(CompileErrorM 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) =
  r
-> ParamFilters
-> Variance
-> ParamName
-> TypeInstance
-> m (MergeTree InferredTypeGuess)
forall (m :: * -> *) r.
(CompileErrorM 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) =
  r
-> ParamFilters
-> Variance
-> TypeInstance
-> ParamName
-> m (MergeTree InferredTypeGuess)
forall (m :: * -> *) r.
(CompileErrorM 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) =
  r
-> ParamFilters
-> Variance
-> ParamName
-> ParamName
-> m (MergeTree InferredTypeGuess)
forall (m :: * -> *) r.
(CompileErrorM m, TypeResolver r) =>
r
-> ParamFilters
-> Variance
-> ParamName
-> ParamName
-> m (MergeTree InferredTypeGuess)
checkParamToParam r
r ParamFilters
f Variance
v ParamName
p1 ParamName
p2

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

checkParamToInstance :: (CompileErrorM m, TypeResolver r) =>
  r -> ParamFilters -> Variance -> ParamName -> TypeInstance -> m (MergeTree InferredTypeGuess)
checkParamToInstance :: 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.
  [m (MergeTree InferredTypeGuess)]
-> m (MergeTree InferredTypeGuess)
forall a (m :: * -> *).
(PreserveMerge a, CompileErrorM m) =>
[m a] -> m a
mergeAllM [
      r
-> ParamFilters
-> Variance
-> ParamName
-> TypeInstance
-> m (MergeTree InferredTypeGuess)
forall (m :: * -> *) r.
(CompileErrorM m, TypeResolver r) =>
r
-> ParamFilters
-> Variance
-> ParamName
-> TypeInstance
-> m (MergeTree InferredTypeGuess)
checkParamToInstance r
r ParamFilters
f Variance
Covariant     ParamName
n1 TypeInstance
t2,
      r
-> ParamFilters
-> Variance
-> ParamName
-> TypeInstance
-> m (MergeTree InferredTypeGuess)
forall (m :: * -> *) r.
(CompileErrorM 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 <- ([TypeFilter] -> [TypeFilter]) -> m [TypeFilter] -> m [TypeFilter]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((TypeFilter -> Bool) -> [TypeFilter] -> [TypeFilter]
forall a. (a -> Bool) -> [a] -> [a]
filter TypeFilter -> Bool
isTypeFilter) (m [TypeFilter] -> m [TypeFilter])
-> m [TypeFilter] -> m [TypeFilter]
forall a b. (a -> b) -> a -> b
$ ParamFilters
f ParamFilters -> ParamName -> m [TypeFilter]
forall (m :: * -> *).
CompileErrorM m =>
ParamFilters -> ParamName -> m [TypeFilter]
`filterLookup` ParamName
n1
  [m (MergeTree InferredTypeGuess)]
-> m (MergeTree InferredTypeGuess)
forall a (m :: * -> *).
(PreserveMerge a, CompileErrorM m) =>
[m a] -> m a
mergeAnyM ((TypeFilter -> m (MergeTree InferredTypeGuess))
-> [TypeFilter] -> [m (MergeTree InferredTypeGuess)]
forall a b. (a -> b) -> [a] -> [b]
map TypeFilter -> m (MergeTree InferredTypeGuess)
forall (m :: * -> *).
CompileErrorM m =>
TypeFilter -> m (MergeTree InferredTypeGuess)
checkConstraintToInstance [TypeFilter]
cs2) m (MergeTree InferredTypeGuess)
-> String -> m (MergeTree InferredTypeGuess)
forall (m :: * -> *) a. CompileErrorM m => m a -> String -> m a
<!!
    (String
"No filters imply " String -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeInstance -> String
forall a. Show a => a -> String
show TypeInstance
t2 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" <- " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ParamName -> String
forall a. Show a => a -> String
show ParamName
n1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" in " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Variance -> String
forall a. Show a => a -> String
show Variance
v String -> ShowS
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
      r
-> ParamFilters
-> Variance
-> GeneralInstance
-> GeneralInstance
-> m (MergeTree InferredTypeGuess)
forall (m :: * -> *) r.
(CompileErrorM m, TypeResolver r) =>
r
-> ParamFilters
-> Variance
-> GeneralInstance
-> GeneralInstance
-> m (MergeTree InferredTypeGuess)
checkGeneralMatch r
r ParamFilters
f Variance
v GeneralInstance
t (TypeInstanceOrParam -> GeneralInstance
forall a. (Eq a, Ord a) => a -> GeneralType a
singleType (TypeInstanceOrParam -> GeneralInstance)
-> TypeInstanceOrParam -> GeneralInstance
forall a b. (a -> b) -> a -> b
$ TypeInstance -> TypeInstanceOrParam
JustTypeInstance TypeInstance
t2)
    checkConstraintToInstance TypeFilter
f2 =
      -- x -> F cannot imply T -> x
      String -> m (MergeTree InferredTypeGuess)
forall (m :: * -> *) a. CompileErrorM m => String -> m a
compileErrorM (String -> m (MergeTree InferredTypeGuess))
-> String -> m (MergeTree InferredTypeGuess)
forall a b. (a -> b) -> a -> b
$ String
"Constraint " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ParamName -> TypeFilter -> String
viewTypeFilter ParamName
n1 TypeFilter
f2 String -> ShowS
forall a. [a] -> [a] -> [a]
++
                      String
" does not imply " String -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeInstance -> String
forall a. Show a => a -> String
show TypeInstance
t2 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" <- " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ParamName -> String
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 <- ([TypeFilter] -> [TypeFilter]) -> m [TypeFilter] -> m [TypeFilter]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((TypeFilter -> Bool) -> [TypeFilter] -> [TypeFilter]
forall a. (a -> Bool) -> [a] -> [a]
filter TypeFilter -> Bool
isTypeFilter) (m [TypeFilter] -> m [TypeFilter])
-> m [TypeFilter] -> m [TypeFilter]
forall a b. (a -> b) -> a -> b
$ ParamFilters
f ParamFilters -> ParamName -> m [TypeFilter]
forall (m :: * -> *).
CompileErrorM m =>
ParamFilters -> ParamName -> m [TypeFilter]
`filterLookup` ParamName
n1
  [m (MergeTree InferredTypeGuess)]
-> m (MergeTree InferredTypeGuess)
forall a (m :: * -> *).
(PreserveMerge a, CompileErrorM m) =>
[m a] -> m a
mergeAnyM ((TypeFilter -> m (MergeTree InferredTypeGuess))
-> [TypeFilter] -> [m (MergeTree InferredTypeGuess)]
forall a b. (a -> b) -> [a] -> [b]
map TypeFilter -> m (MergeTree InferredTypeGuess)
forall (m :: * -> *).
CompileErrorM m =>
TypeFilter -> m (MergeTree InferredTypeGuess)
checkConstraintToInstance [TypeFilter]
cs1) m (MergeTree InferredTypeGuess)
-> String -> m (MergeTree InferredTypeGuess)
forall (m :: * -> *) a. CompileErrorM m => m a -> String -> m a
<!!
    (String
"No filters imply " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ParamName -> String
forall a. Show a => a -> String
show ParamName
n1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" -> " String -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeInstance -> String
forall a. Show a => a -> String
show TypeInstance
t2 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" in " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Variance -> String
forall a. Show a => a -> String
show Variance
v String -> ShowS
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
      r
-> ParamFilters
-> Variance
-> GeneralInstance
-> GeneralInstance
-> m (MergeTree InferredTypeGuess)
forall (m :: * -> *) r.
(CompileErrorM m, TypeResolver r) =>
r
-> ParamFilters
-> Variance
-> GeneralInstance
-> GeneralInstance
-> m (MergeTree InferredTypeGuess)
checkGeneralMatch r
r ParamFilters
f Variance
v GeneralInstance
t (TypeInstanceOrParam -> GeneralInstance
forall a. (Eq a, Ord a) => a -> GeneralType a
singleType (TypeInstanceOrParam -> GeneralInstance)
-> TypeInstanceOrParam -> GeneralInstance
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
      String -> m (MergeTree InferredTypeGuess)
forall (m :: * -> *) a. CompileErrorM m => String -> m a
compileErrorM (String -> m (MergeTree InferredTypeGuess))
-> String -> m (MergeTree InferredTypeGuess)
forall a b. (a -> b) -> a -> b
$ String
"Constraint " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ParamName -> TypeFilter -> String
viewTypeFilter ParamName
n1 TypeFilter
f2 String -> ShowS
forall a. [a] -> [a] -> [a]
++
                      String
" does not imply " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ParamName -> String
forall a. Show a => a -> String
show ParamName
n1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" -> " String -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeInstance -> String
forall a. Show a => a -> String
show TypeInstance
t2

checkInstanceToParam :: (CompileErrorM m, TypeResolver r) =>
  r -> ParamFilters -> Variance -> TypeInstance -> ParamName -> m (MergeTree InferredTypeGuess)
checkInstanceToParam :: 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.
  [m (MergeTree InferredTypeGuess)]
-> m (MergeTree InferredTypeGuess)
forall a (m :: * -> *).
(PreserveMerge a, CompileErrorM m) =>
[m a] -> m a
mergeAllM [
      r
-> ParamFilters
-> Variance
-> TypeInstance
-> ParamName
-> m (MergeTree InferredTypeGuess)
forall (m :: * -> *) r.
(CompileErrorM m, TypeResolver r) =>
r
-> ParamFilters
-> Variance
-> TypeInstance
-> ParamName
-> m (MergeTree InferredTypeGuess)
checkInstanceToParam r
r ParamFilters
f Variance
Covariant     TypeInstance
t1 ParamName
n2,
      r
-> ParamFilters
-> Variance
-> TypeInstance
-> ParamName
-> m (MergeTree InferredTypeGuess)
forall (m :: * -> *) r.
(CompileErrorM 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 <- ([TypeFilter] -> [TypeFilter]) -> m [TypeFilter] -> m [TypeFilter]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((TypeFilter -> Bool) -> [TypeFilter] -> [TypeFilter]
forall a. (a -> Bool) -> [a] -> [a]
filter TypeFilter -> Bool
isTypeFilter) (m [TypeFilter] -> m [TypeFilter])
-> m [TypeFilter] -> m [TypeFilter]
forall a b. (a -> b) -> a -> b
$ ParamFilters
f ParamFilters -> ParamName -> m [TypeFilter]
forall (m :: * -> *).
CompileErrorM m =>
ParamFilters -> ParamName -> m [TypeFilter]
`filterLookup` ParamName
n2
  [m (MergeTree InferredTypeGuess)]
-> m (MergeTree InferredTypeGuess)
forall a (m :: * -> *).
(PreserveMerge a, CompileErrorM m) =>
[m a] -> m a
mergeAnyM ((TypeFilter -> m (MergeTree InferredTypeGuess))
-> [TypeFilter] -> [m (MergeTree InferredTypeGuess)]
forall a b. (a -> b) -> [a] -> [b]
map TypeFilter -> m (MergeTree InferredTypeGuess)
forall (m :: * -> *).
CompileErrorM m =>
TypeFilter -> m (MergeTree InferredTypeGuess)
checkInstanceToConstraint [TypeFilter]
cs1) m (MergeTree InferredTypeGuess)
-> String -> m (MergeTree InferredTypeGuess)
forall (m :: * -> *) a. CompileErrorM m => m a -> String -> m a
<!!
    (String
"No filters imply " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ParamName -> String
forall a. Show a => a -> String
show ParamName
n2 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" <- " String -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeInstance -> String
forall a. Show a => a -> String
show TypeInstance
t1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" in " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Variance -> String
forall a. Show a => a -> String
show Variance
v String -> ShowS
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
      r
-> ParamFilters
-> Variance
-> GeneralInstance
-> GeneralInstance
-> m (MergeTree InferredTypeGuess)
forall (m :: * -> *) r.
(CompileErrorM m, TypeResolver r) =>
r
-> ParamFilters
-> Variance
-> GeneralInstance
-> GeneralInstance
-> m (MergeTree InferredTypeGuess)
checkGeneralMatch r
r ParamFilters
f Variance
v (TypeInstanceOrParam -> GeneralInstance
forall a. (Eq a, Ord a) => a -> GeneralType a
singleType (TypeInstanceOrParam -> GeneralInstance)
-> TypeInstanceOrParam -> GeneralInstance
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
      String -> m (MergeTree InferredTypeGuess)
forall (m :: * -> *) a. CompileErrorM m => String -> m a
compileErrorM (String -> m (MergeTree InferredTypeGuess))
-> String -> m (MergeTree InferredTypeGuess)
forall a b. (a -> b) -> a -> b
$ String
"Constraint " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ParamName -> TypeFilter -> String
viewTypeFilter ParamName
n2 TypeFilter
f2 String -> ShowS
forall a. [a] -> [a] -> [a]
++
                      String
" does not imply " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ParamName -> String
forall a. Show a => a -> String
show ParamName
n2 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" <- " String -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeInstance -> String
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 <- ([TypeFilter] -> [TypeFilter]) -> m [TypeFilter] -> m [TypeFilter]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((TypeFilter -> Bool) -> [TypeFilter] -> [TypeFilter]
forall a. (a -> Bool) -> [a] -> [a]
filter TypeFilter -> Bool
isTypeFilter) (m [TypeFilter] -> m [TypeFilter])
-> m [TypeFilter] -> m [TypeFilter]
forall a b. (a -> b) -> a -> b
$ ParamFilters
f ParamFilters -> ParamName -> m [TypeFilter]
forall (m :: * -> *).
CompileErrorM m =>
ParamFilters -> ParamName -> m [TypeFilter]
`filterLookup` ParamName
n2
  [m (MergeTree InferredTypeGuess)]
-> m (MergeTree InferredTypeGuess)
forall a (m :: * -> *).
(PreserveMerge a, CompileErrorM m) =>
[m a] -> m a
mergeAnyM ((TypeFilter -> m (MergeTree InferredTypeGuess))
-> [TypeFilter] -> [m (MergeTree InferredTypeGuess)]
forall a b. (a -> b) -> [a] -> [b]
map TypeFilter -> m (MergeTree InferredTypeGuess)
forall (m :: * -> *).
CompileErrorM m =>
TypeFilter -> m (MergeTree InferredTypeGuess)
checkInstanceToConstraint [TypeFilter]
cs2) m (MergeTree InferredTypeGuess)
-> String -> m (MergeTree InferredTypeGuess)
forall (m :: * -> *) a. CompileErrorM m => m a -> String -> m a
<!!
    (String
"No filters imply " String -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeInstance -> String
forall a. Show a => a -> String
show TypeInstance
t1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" -> " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ParamName -> String
forall a. Show a => a -> String
show ParamName
n2 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" in " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Variance -> String
forall a. Show a => a -> String
show Variance
v String -> ShowS
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
      r
-> ParamFilters
-> Variance
-> GeneralInstance
-> GeneralInstance
-> m (MergeTree InferredTypeGuess)
forall (m :: * -> *) r.
(CompileErrorM m, TypeResolver r) =>
r
-> ParamFilters
-> Variance
-> GeneralInstance
-> GeneralInstance
-> m (MergeTree InferredTypeGuess)
checkGeneralMatch r
r ParamFilters
f Variance
v (TypeInstanceOrParam -> GeneralInstance
forall a. (Eq a, Ord a) => a -> GeneralType a
singleType (TypeInstanceOrParam -> GeneralInstance)
-> TypeInstanceOrParam -> GeneralInstance
forall a b. (a -> b) -> a -> b
$ TypeInstance -> TypeInstanceOrParam
JustTypeInstance TypeInstance
t1) GeneralInstance
t
    checkInstanceToConstraint TypeFilter
f2 =
      -- x -> F cannot imply T -> x
      String -> m (MergeTree InferredTypeGuess)
forall (m :: * -> *) a. CompileErrorM m => String -> m a
compileErrorM (String -> m (MergeTree InferredTypeGuess))
-> String -> m (MergeTree InferredTypeGuess)
forall a b. (a -> b) -> a -> b
$ String
"Constraint " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ParamName -> TypeFilter -> String
viewTypeFilter ParamName
n2 TypeFilter
f2 String -> ShowS
forall a. [a] -> [a] -> [a]
++
                      String
" does not imply " String -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeInstance -> String
forall a. Show a => a -> String
show TypeInstance
t1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" -> " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ParamName -> String
forall a. Show a => a -> String
show ParamName
n2

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

validateGeneralInstance :: (CompileErrorM m, TypeResolver r) =>
  r -> ParamFilters -> GeneralInstance -> m ()
validateGeneralInstance :: r -> ParamFilters -> GeneralInstance -> m ()
validateGeneralInstance r
r ParamFilters
f = ([m ()] -> m ())
-> ([m ()] -> m ())
-> (T GeneralInstance -> m ())
-> GeneralInstance
-> m ()
forall a b.
PreserveMerge a =>
([b] -> b) -> ([b] -> b) -> (T a -> b) -> a -> b
reduceMergeTree [m ()] -> m ()
forall (f :: * -> *) (m :: * -> *) a.
(Foldable f, CompileErrorM m) =>
f (m a) -> m ()
collectAllM_ [m ()] -> m ()
forall (f :: * -> *) (m :: * -> *) a.
(Foldable f, CompileErrorM m) =>
f (m a) -> m ()
collectAllM_ T GeneralInstance -> m ()
forall (m :: * -> *).
CompileErrorM m =>
TypeInstanceOrParam -> m ()
validateSingle where
  validateSingle :: TypeInstanceOrParam -> m ()
validateSingle (JustTypeInstance TypeInstance
t) = r -> ParamFilters -> TypeInstance -> m ()
forall (m :: * -> *) r.
(CompileErrorM m, TypeResolver r) =>
r -> ParamFilters -> TypeInstance -> m ()
validateTypeInstance r
r ParamFilters
f TypeInstance
t
  validateSingle (JustParamName Bool
_ ParamName
n) = Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ ParamName
n ParamName -> ParamFilters -> Bool
forall k a. Ord k => k -> Map k a -> Bool
`Map.member` ParamFilters
f) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$
      String -> m ()
forall (m :: * -> *) a. CompileErrorM m => String -> m a
compileErrorM (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$ String
"Param " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ParamName -> String
forall a. Show a => a -> String
show ParamName
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" does not exist"
  validateSingle (JustInferredType ParamName
n) = String -> m ()
forall (m :: * -> *) a. CompileErrorM m => String -> m a
compileErrorM (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$ String
"Inferred param " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ParamName -> String
forall a. Show a => a -> String
show ParamName
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" is not allowed here"

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

validateDefinesInstance :: (CompileErrorM m, TypeResolver r) =>
  r -> ParamFilters -> DefinesInstance -> m ()
validateDefinesInstance :: r -> ParamFilters -> DefinesInstance -> m ()
validateDefinesInstance r
r ParamFilters
f t :: DefinesInstance
t@(DefinesInstance CategoryName
_ InstanceParams
ps) = do
  InstanceFilters
fa <- r -> DefinesInstance -> m InstanceFilters
forall r (m :: * -> *).
(TypeResolver r, CompileErrorM m) =>
r -> DefinesInstance -> m InstanceFilters
trDefinesFilters r
r DefinesInstance
t
  (GeneralInstance -> [TypeFilter] -> m ())
-> InstanceParams -> InstanceFilters -> m ()
forall a b (m :: * -> *) c.
(Show a, Show b, CompileErrorM m) =>
(a -> b -> m c) -> Positional a -> Positional b -> m ()
processPairs_ (r -> ParamFilters -> GeneralInstance -> [TypeFilter] -> m ()
forall (m :: * -> *) r.
(CompileErrorM m, TypeResolver r) =>
r -> ParamFilters -> GeneralInstance -> [TypeFilter] -> m ()
validateAssignment r
r ParamFilters
f) InstanceParams
ps InstanceFilters
fa
  (GeneralInstance -> m ()) -> [GeneralInstance] -> m ()
forall (m :: * -> *) a b.
CompileErrorM m =>
(a -> m b) -> [a] -> m ()
mapErrorsM_ (r -> ParamFilters -> GeneralInstance -> m ()
forall (m :: * -> *) r.
(CompileErrorM m, TypeResolver r) =>
r -> ParamFilters -> GeneralInstance -> m ()
validateGeneralInstance r
r ParamFilters
f) (InstanceParams -> [GeneralInstance]
forall a. Positional a -> [a]
pValues InstanceParams
ps) m () -> String -> m ()
forall (m :: * -> *) a. CompileErrorM m => m a -> String -> m a
<?? (String
"In " String -> ShowS
forall a. [a] -> [a] -> [a]
++ DefinesInstance -> String
forall a. Show a => a -> String
show DefinesInstance
t)

validateTypeFilter :: (CompileErrorM m, TypeResolver r) =>
  r -> ParamFilters -> TypeFilter -> m ()
validateTypeFilter :: r -> ParamFilters -> TypeFilter -> m ()
validateTypeFilter r
r ParamFilters
f (TypeFilter FilterDirection
_ GeneralInstance
t)  = r -> ParamFilters -> GeneralInstance -> m ()
forall (m :: * -> *) r.
(CompileErrorM m, TypeResolver r) =>
r -> ParamFilters -> GeneralInstance -> m ()
validateGeneralInstance r
r ParamFilters
f GeneralInstance
t
validateTypeFilter r
r ParamFilters
f (DefinesFilter DefinesInstance
t) = r -> ParamFilters -> DefinesInstance -> m ()
forall (m :: * -> *) r.
(CompileErrorM m, TypeResolver r) =>
r -> ParamFilters -> DefinesInstance -> m ()
validateDefinesInstance r
r ParamFilters
f DefinesInstance
t

validateAssignment :: (CompileErrorM m, TypeResolver r) =>
  r -> ParamFilters -> GeneralInstance -> [TypeFilter] -> m ()
validateAssignment :: r -> ParamFilters -> GeneralInstance -> [TypeFilter] -> m ()
validateAssignment r
r ParamFilters
f GeneralInstance
t [TypeFilter]
fs = (TypeFilter -> m ()) -> [TypeFilter] -> m ()
forall (m :: * -> *) a b.
CompileErrorM m =>
(a -> m b) -> [a] -> m ()
mapErrorsM_ TypeFilter -> m ()
forall (m :: * -> *). CompileErrorM m => TypeFilter -> m ()
checkWithMessage [TypeFilter]
fs where
  checkWithMessage :: TypeFilter -> m ()
checkWithMessage TypeFilter
f2 = GeneralInstance -> TypeFilter -> m ()
forall (m :: * -> *).
CompileErrorM m =>
GeneralInstance -> TypeFilter -> m ()
checkFilter GeneralInstance
t TypeFilter
f2 m () -> String -> m ()
forall (m :: * -> *) a. CompileErrorM m => m a -> String -> m a
<?? (String
"In verification of filter " String -> ShowS
forall a. [a] -> [a] -> [a]
++ GeneralInstance -> String
forall a. Show a => a -> String
show GeneralInstance
t String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeFilter -> String
forall a. Show a => a -> String
show TypeFilter
f2)
  checkFilter :: GeneralInstance -> TypeFilter -> m ()
checkFilter GeneralInstance
t1 (TypeFilter FilterDirection
FilterRequires GeneralInstance
t2) =
    m (MergeTree InferredTypeGuess) -> m ()
forall (m :: * -> *).
CompileErrorM m =>
m (MergeTree InferredTypeGuess) -> m ()
noInferredTypes (m (MergeTree InferredTypeGuess) -> m ())
-> m (MergeTree InferredTypeGuess) -> m ()
forall a b. (a -> b) -> a -> b
$ r
-> ParamFilters
-> Variance
-> GeneralInstance
-> GeneralInstance
-> m (MergeTree InferredTypeGuess)
forall (m :: * -> *) r.
(CompileErrorM 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) =
    m (MergeTree InferredTypeGuess) -> m ()
forall (m :: * -> *).
CompileErrorM m =>
m (MergeTree InferredTypeGuess) -> m ()
noInferredTypes (m (MergeTree InferredTypeGuess) -> m ())
-> m (MergeTree InferredTypeGuess) -> m ()
forall a b. (a -> b) -> a -> b
$ r
-> ParamFilters
-> Variance
-> GeneralInstance
-> GeneralInstance
-> m (MergeTree InferredTypeGuess)
forall (m :: * -> *) r.
(CompileErrorM 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' <- GeneralInstance -> m (T GeneralInstance)
forall a (m :: * -> *).
(PreserveMerge a, CompileErrorM m) =>
a -> m (T a)
matchOnlyLeaf GeneralInstance
t1 m TypeInstanceOrParam -> String -> m TypeInstanceOrParam
forall (m :: * -> *) a. CompileErrorM m => m a -> String -> m a
<!! (String
"Merged type " String -> ShowS
forall a. [a] -> [a] -> [a]
++ GeneralInstance -> String
forall a. Show a => a -> String
show GeneralInstance
t1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" cannot satisfy defines constraint " String -> ShowS
forall a. [a] -> [a] -> [a]
++ DefinesInstance -> String
forall a. Show a => a -> String
show DefinesInstance
t2)
    DefinesInstance -> TypeInstanceOrParam -> m ()
forall (m :: * -> *).
CompileErrorM m =>
DefinesInstance -> TypeInstanceOrParam -> m ()
checkDefinesFilter DefinesInstance
t2 TypeInstanceOrParam
t1'
  checkDefinesFilter :: DefinesInstance -> TypeInstanceOrParam -> m ()
checkDefinesFilter f2 :: DefinesInstance
f2@(DefinesInstance CategoryName
n2 InstanceParams
_) (JustTypeInstance TypeInstance
t1) = do
    InstanceParams
ps1' <- r -> TypeInstance -> CategoryName -> m InstanceParams
forall r (m :: * -> *).
(TypeResolver r, CompileErrorM m) =>
r -> TypeInstance -> CategoryName -> m InstanceParams
trDefines r
r TypeInstance
t1 CategoryName
n2
    r -> ParamFilters -> DefinesInstance -> DefinesInstance -> m ()
forall (m :: * -> *) r.
(CompileErrorM m, TypeResolver r) =>
r -> ParamFilters -> DefinesInstance -> DefinesInstance -> m ()
checkDefinesMatch r
r ParamFilters
f DefinesInstance
f2 (CategoryName -> InstanceParams -> DefinesInstance
DefinesInstance CategoryName
n2 InstanceParams
ps1')
  checkDefinesFilter DefinesInstance
f2 (JustParamName Bool
_ ParamName
n1) = do
      [DefinesInstance]
fs1 <- ([TypeFilter] -> [DefinesInstance])
-> m [TypeFilter] -> m [DefinesInstance]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((TypeFilter -> DefinesInstance)
-> [TypeFilter] -> [DefinesInstance]
forall a b. (a -> b) -> [a] -> [b]
map TypeFilter -> DefinesInstance
dfType ([TypeFilter] -> [DefinesInstance])
-> ([TypeFilter] -> [TypeFilter])
-> [TypeFilter]
-> [DefinesInstance]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TypeFilter -> Bool) -> [TypeFilter] -> [TypeFilter]
forall a. (a -> Bool) -> [a] -> [a]
filter TypeFilter -> Bool
isDefinesFilter) (m [TypeFilter] -> m [DefinesInstance])
-> m [TypeFilter] -> m [DefinesInstance]
forall a b. (a -> b) -> a -> b
$ ParamFilters
f ParamFilters -> ParamName -> m [TypeFilter]
forall (m :: * -> *).
CompileErrorM m =>
ParamFilters -> ParamName -> m [TypeFilter]
`filterLookup` ParamName
n1
      ([m ()] -> m ()
forall (f :: * -> *) (m :: * -> *) a.
(Foldable f, CompileErrorM m) =>
f (m a) -> m ()
collectFirstM_ ([m ()] -> m ()) -> [m ()] -> m ()
forall a b. (a -> b) -> a -> b
$ (DefinesInstance -> m ()) -> [DefinesInstance] -> [m ()]
forall a b. (a -> b) -> [a] -> [b]
map (r -> ParamFilters -> DefinesInstance -> DefinesInstance -> m ()
forall (m :: * -> *) r.
(CompileErrorM m, TypeResolver r) =>
r -> ParamFilters -> DefinesInstance -> DefinesInstance -> m ()
checkDefinesMatch r
r ParamFilters
f DefinesInstance
f2) [DefinesInstance]
fs1) m () -> String -> m ()
forall (m :: * -> *) a. CompileErrorM m => m a -> String -> m a
<!!
        (String
"No filters imply " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ParamName -> String
forall a. Show a => a -> String
show ParamName
n1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" defines " String -> ShowS
forall a. [a] -> [a] -> [a]
++ DefinesInstance -> String
forall a. Show a => a -> String
show DefinesInstance
f2)
  checkDefinesFilter DefinesInstance
_ (JustInferredType ParamName
n) =
    String -> m ()
forall (m :: * -> *) a. CompileErrorM m => String -> m a
compileErrorM (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$ String
"Inferred param " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ParamName -> String
forall a. Show a => a -> String
show ParamName
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" is not allowed here"

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

validateInstanceVariance :: (CompileErrorM m, TypeResolver r) =>
  r -> ParamVariances -> Variance -> GeneralInstance -> m ()
validateInstanceVariance :: r -> ParamVariances -> Variance -> GeneralInstance -> m ()
validateInstanceVariance r
r ParamVariances
vm Variance
v = ([m ()] -> m ())
-> ([m ()] -> m ())
-> (T GeneralInstance -> m ())
-> GeneralInstance
-> m ()
forall a b.
PreserveMerge a =>
([b] -> b) -> ([b] -> b) -> (T a -> b) -> a -> b
reduceMergeTree [m ()] -> m ()
forall (f :: * -> *) (m :: * -> *) a.
(Foldable f, CompileErrorM m) =>
f (m a) -> m ()
collectAllM_ [m ()] -> m ()
forall (f :: * -> *) (m :: * -> *) a.
(Foldable f, CompileErrorM m) =>
f (m a) -> m ()
collectAllM_ T GeneralInstance -> m ()
forall (m :: * -> *).
CompileErrorM m =>
TypeInstanceOrParam -> m ()
validateSingle where
  validateSingle :: TypeInstanceOrParam -> m ()
validateSingle (JustTypeInstance (TypeInstance CategoryName
n InstanceParams
ps)) = do
    InstanceVariances
vs <- r -> CategoryName -> m InstanceVariances
forall r (m :: * -> *).
(TypeResolver r, CompileErrorM m) =>
r -> CategoryName -> m InstanceVariances
trVariance r
r CategoryName
n
    [(Variance, GeneralInstance)]
paired <- (Variance -> GeneralInstance -> m (Variance, GeneralInstance))
-> InstanceVariances
-> InstanceParams
-> m [(Variance, GeneralInstance)]
forall a b (m :: * -> *) c.
(Show a, Show b, CompileErrorM m) =>
(a -> b -> m c) -> Positional a -> Positional b -> m [c]
processPairs Variance -> GeneralInstance -> m (Variance, GeneralInstance)
forall (m :: * -> *) a b. Monad m => a -> b -> m (a, b)
alwaysPair InstanceVariances
vs InstanceParams
ps
    ((Variance, GeneralInstance) -> m ())
-> [(Variance, GeneralInstance)] -> m ()
forall (m :: * -> *) a b.
CompileErrorM m =>
(a -> m b) -> [a] -> m ()
mapErrorsM_ (\(Variance
v2,GeneralInstance
p) -> r -> ParamVariances -> Variance -> GeneralInstance -> m ()
forall (m :: * -> *) r.
(CompileErrorM 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 ParamName -> ParamVariances -> Maybe Variance
forall k a. Ord k => k -> Map k a -> Maybe a
`Map.lookup` ParamVariances
vm of
        Maybe Variance
Nothing -> String -> m ()
forall (m :: * -> *) a. CompileErrorM m => String -> m a
compileErrorM (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$ String
"Param " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ParamName -> String
forall a. Show a => a -> String
show ParamName
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" is undefined"
        (Just Variance
v0) -> Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Variance
v0 Variance -> Variance -> Bool
`allowsVariance` Variance
v) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$
                          String -> m ()
forall (m :: * -> *) a. CompileErrorM m => String -> m a
compileErrorM (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$ String
"Param " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ParamName -> String
forall a. Show a => a -> String
show ParamName
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" cannot be " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Variance -> String
forall a. Show a => a -> String
show Variance
v
  validateSingle (JustInferredType ParamName
n) =
    String -> m ()
forall (m :: * -> *) a. CompileErrorM m => String -> m a
compileErrorM (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$ String
"Inferred param " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ParamName -> String
forall a. Show a => a -> String
show ParamName
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" is not allowed here"

validateDefinesVariance :: (CompileErrorM m, TypeResolver r) =>
  r -> ParamVariances -> Variance -> DefinesInstance -> m ()
validateDefinesVariance :: r -> ParamVariances -> Variance -> DefinesInstance -> m ()
validateDefinesVariance r
r ParamVariances
vm Variance
v (DefinesInstance CategoryName
n InstanceParams
ps) = do
  InstanceVariances
vs <- r -> CategoryName -> m InstanceVariances
forall r (m :: * -> *).
(TypeResolver r, CompileErrorM m) =>
r -> CategoryName -> m InstanceVariances
trVariance r
r CategoryName
n
  [(Variance, GeneralInstance)]
paired <- (Variance -> GeneralInstance -> m (Variance, GeneralInstance))
-> InstanceVariances
-> InstanceParams
-> m [(Variance, GeneralInstance)]
forall a b (m :: * -> *) c.
(Show a, Show b, CompileErrorM m) =>
(a -> b -> m c) -> Positional a -> Positional b -> m [c]
processPairs Variance -> GeneralInstance -> m (Variance, GeneralInstance)
forall (m :: * -> *) a b. Monad m => a -> b -> m (a, b)
alwaysPair InstanceVariances
vs InstanceParams
ps
  ((Variance, GeneralInstance) -> m ())
-> [(Variance, GeneralInstance)] -> m ()
forall (m :: * -> *) a b.
CompileErrorM m =>
(a -> m b) -> [a] -> m ()
mapErrorsM_ (\(Variance
v2,GeneralInstance
p) -> r -> ParamVariances -> Variance -> GeneralInstance -> m ()
forall (m :: * -> *) r.
(CompileErrorM 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

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

uncheckedSubInstance :: CompileErrorM m => (ParamName -> m GeneralInstance) ->
  GeneralInstance -> m GeneralInstance
uncheckedSubInstance :: (ParamName -> m GeneralInstance)
-> GeneralInstance -> m GeneralInstance
uncheckedSubInstance ParamName -> m GeneralInstance
replace = ([m GeneralInstance] -> m GeneralInstance)
-> ([m GeneralInstance] -> m GeneralInstance)
-> (T GeneralInstance -> m GeneralInstance)
-> GeneralInstance
-> m GeneralInstance
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 T GeneralInstance -> m GeneralInstance
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 = ([GeneralInstance] -> GeneralInstance)
-> m [GeneralInstance] -> m GeneralInstance
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [GeneralInstance] -> GeneralInstance
forall a (f :: * -> *). (Mergeable a, Foldable f) => f a -> a
mergeAny (m [GeneralInstance] -> m GeneralInstance)
-> ([m GeneralInstance] -> m [GeneralInstance])
-> [m GeneralInstance]
-> m GeneralInstance
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [m GeneralInstance] -> m [GeneralInstance]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence
  subAll :: [m GeneralInstance] -> m GeneralInstance
subAll = ([GeneralInstance] -> GeneralInstance)
-> m [GeneralInstance] -> m GeneralInstance
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [GeneralInstance] -> GeneralInstance
forall a (f :: * -> *). (Mergeable a, Foldable f) => f a -> a
mergeAll (m [GeneralInstance] -> m GeneralInstance)
-> ([m GeneralInstance] -> m [GeneralInstance])
-> [m GeneralInstance]
-> m GeneralInstance
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [m GeneralInstance] -> m [GeneralInstance]
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
True ParamName
_) = GeneralInstance -> m GeneralInstance
forall (m :: * -> *) a. Monad m => a -> m a
return (GeneralInstance -> m GeneralInstance)
-> GeneralInstance -> m GeneralInstance
forall a b. (a -> b) -> a -> b
$ TypeInstanceOrParam -> GeneralInstance
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)     = (TypeInstance -> GeneralInstance)
-> m TypeInstance -> m GeneralInstance
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (TypeInstanceOrParam -> GeneralInstance
forall a. (Eq a, Ord a) => a -> GeneralType a
singleType (TypeInstanceOrParam -> GeneralInstance)
-> (TypeInstance -> TypeInstanceOrParam)
-> TypeInstance
-> GeneralInstance
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeInstance -> TypeInstanceOrParam
JustTypeInstance) (m TypeInstance -> m GeneralInstance)
-> m TypeInstance -> m GeneralInstance
forall a b. (a -> b) -> a -> b
$ (ParamName -> m GeneralInstance) -> TypeInstance -> m TypeInstance
forall (m :: * -> *).
CompileErrorM m =>
(ParamName -> m GeneralInstance) -> TypeInstance -> m TypeInstance
uncheckedSubSingle ParamName -> m GeneralInstance
replace TypeInstance
t

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

uncheckedSubFilter :: CompileErrorM m =>
  (ParamName -> m GeneralInstance) -> TypeFilter -> m TypeFilter
uncheckedSubFilter :: (ParamName -> m GeneralInstance) -> TypeFilter -> m TypeFilter
uncheckedSubFilter ParamName -> m GeneralInstance
replace (TypeFilter FilterDirection
d GeneralInstance
t) = do
  GeneralInstance
t' <- (ParamName -> m GeneralInstance)
-> GeneralInstance -> m GeneralInstance
forall (m :: * -> *).
CompileErrorM m =>
(ParamName -> m GeneralInstance)
-> GeneralInstance -> m GeneralInstance
uncheckedSubInstance ParamName -> m GeneralInstance
replace GeneralInstance
t
  TypeFilter -> m TypeFilter
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' <- (GeneralInstance -> m GeneralInstance)
-> [GeneralInstance] -> m [GeneralInstance]
forall (m :: * -> *) a b.
CompileErrorM m =>
(a -> m b) -> [a] -> m [b]
mapErrorsM ((ParamName -> m GeneralInstance)
-> GeneralInstance -> m GeneralInstance
forall (m :: * -> *).
CompileErrorM m =>
(ParamName -> m GeneralInstance)
-> GeneralInstance -> m GeneralInstance
uncheckedSubInstance ParamName -> m GeneralInstance
replace) (InstanceParams -> [GeneralInstance]
forall a. Positional a -> [a]
pValues InstanceParams
ts)
  TypeFilter -> m TypeFilter
forall (m :: * -> *) a. Monad m => a -> m a
return (DefinesInstance -> TypeFilter
DefinesFilter (CategoryName -> InstanceParams -> DefinesInstance
DefinesInstance CategoryName
n ([GeneralInstance] -> InstanceParams
forall a. [a] -> Positional a
Positional [GeneralInstance]
ts')))

uncheckedSubFilters :: CompileErrorM m =>
  (ParamName -> m GeneralInstance) -> ParamFilters -> m ParamFilters
uncheckedSubFilters :: (ParamName -> m GeneralInstance) -> ParamFilters -> m ParamFilters
uncheckedSubFilters ParamName -> m GeneralInstance
replace ParamFilters
fa = do
  [(ParamName, [TypeFilter])]
fa' <- ((ParamName, [TypeFilter]) -> m (ParamName, [TypeFilter]))
-> [(ParamName, [TypeFilter])] -> m [(ParamName, [TypeFilter])]
forall (m :: * -> *) a b.
CompileErrorM m =>
(a -> m b) -> [a] -> m [b]
mapErrorsM (ParamName, [TypeFilter]) -> m (ParamName, [TypeFilter])
forall a. (a, [TypeFilter]) -> m (a, [TypeFilter])
subParam ([(ParamName, [TypeFilter])] -> m [(ParamName, [TypeFilter])])
-> [(ParamName, [TypeFilter])] -> m [(ParamName, [TypeFilter])]
forall a b. (a -> b) -> a -> b
$ ParamFilters -> [(ParamName, [TypeFilter])]
forall k a. Map k a -> [(k, a)]
Map.toList ParamFilters
fa
  ParamFilters -> m ParamFilters
forall (m :: * -> *) a. Monad m => a -> m a
return (ParamFilters -> m ParamFilters) -> ParamFilters -> m ParamFilters
forall a b. (a -> b) -> a -> b
$ [(ParamName, [TypeFilter])] -> ParamFilters
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' <- (TypeFilter -> m TypeFilter) -> [TypeFilter] -> m [TypeFilter]
forall (m :: * -> *) a b.
CompileErrorM m =>
(a -> m b) -> [a] -> m [b]
mapErrorsM ((ParamName -> m GeneralInstance) -> TypeFilter -> m TypeFilter
forall (m :: * -> *).
CompileErrorM m =>
(ParamName -> m GeneralInstance) -> TypeFilter -> m TypeFilter
uncheckedSubFilter ParamName -> m GeneralInstance
replace) [TypeFilter]
fs
      (a, [TypeFilter]) -> m (a, [TypeFilter])
forall (m :: * -> *) a. Monad m => a -> m a
return (a
n,[TypeFilter]
fs')