{- -----------------------------------------------------------------------------
Copyright 2019-2021 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]

module Test.TypeInstance (tests) where

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

import Base.CompilerError
import Base.GeneralType
import Base.Positional
import Base.TrackedErrors
import Base.MergeTree
import Base.Mergeable
import Parser.TypeInstance ()
import Test.Common
import Types.TypeInstance
import Types.Variance


tests :: [IO (TrackedErrors ())]
tests :: [IO (TrackedErrors ())]
tests = [
    String -> GeneralInstance -> IO (TrackedErrors ())
checkParseSuccess
      String
"Type0"
      (forall a. (Eq a, Ord a) => a -> GeneralType a
singleType forall a b. (a -> b) -> a -> b
$ TypeInstance -> TypeInstanceOrParam
JustTypeInstance forall a b. (a -> b) -> a -> b
$ CategoryName -> InstanceParams -> TypeInstance
TypeInstance (String -> CategoryName
CategoryName String
"Type0") (forall a. [a] -> Positional a
Positional [])),
    String -> GeneralInstance -> IO (TrackedErrors ())
checkParseSuccess
      String
"Type0<Type1,Type2>"
      (forall a. (Eq a, Ord a) => a -> GeneralType a
singleType forall a b. (a -> b) -> a -> b
$ TypeInstance -> TypeInstanceOrParam
JustTypeInstance forall a b. (a -> b) -> a -> b
$ CategoryName -> InstanceParams -> TypeInstance
TypeInstance (String -> CategoryName
CategoryName String
"Type0") (forall a. [a] -> Positional a
Positional [
          forall a. (Eq a, Ord a) => a -> GeneralType a
singleType forall a b. (a -> b) -> a -> b
$ TypeInstance -> TypeInstanceOrParam
JustTypeInstance forall a b. (a -> b) -> a -> b
$ CategoryName -> InstanceParams -> TypeInstance
TypeInstance (String -> CategoryName
CategoryName String
"Type1") (forall a. [a] -> Positional a
Positional []),
          forall a. (Eq a, Ord a) => a -> GeneralType a
singleType forall a b. (a -> b) -> a -> b
$ TypeInstance -> TypeInstanceOrParam
JustTypeInstance forall a b. (a -> b) -> a -> b
$ CategoryName -> InstanceParams -> TypeInstance
TypeInstance (String -> CategoryName
CategoryName String
"Type2") (forall a. [a] -> Positional a
Positional [])
        ])),
    String -> GeneralInstance -> IO (TrackedErrors ())
checkParseSuccess
      String
"#x"
      (forall a. (Eq a, Ord a) => a -> GeneralType a
singleType forall a b. (a -> b) -> a -> b
$ Bool -> ParamName -> TypeInstanceOrParam
JustParamName Bool
False forall a b. (a -> b) -> a -> b
$ String -> ParamName
ParamName String
"#x"),
    String -> GeneralInstance -> IO (TrackedErrors ())
checkParseSuccess
      String
"#self"
      (forall a. (Eq a, Ord a) => a -> GeneralType a
singleType forall a b. (a -> b) -> a -> b
$ Bool -> ParamName -> TypeInstanceOrParam
JustParamName Bool
False forall a b. (a -> b) -> a -> b
$ ParamName
ParamSelf),
    String -> GeneralInstance -> IO (TrackedErrors ())
checkParseSuccess
      String
"Type0<#self>"
      (forall a. (Eq a, Ord a) => a -> GeneralType a
singleType forall a b. (a -> b) -> a -> b
$ TypeInstance -> TypeInstanceOrParam
JustTypeInstance forall a b. (a -> b) -> a -> b
$ CategoryName -> InstanceParams -> TypeInstance
TypeInstance (String -> CategoryName
CategoryName String
"Type0") (forall a. [a] -> Positional a
Positional [
          forall a. (Eq a, Ord a) => a -> GeneralType a
singleType forall a b. (a -> b) -> a -> b
$ Bool -> ParamName -> TypeInstanceOrParam
JustParamName Bool
False forall a b. (a -> b) -> a -> b
$ ParamName
ParamSelf
        ])),
    String -> IO (TrackedErrors ())
checkParseFail String
"x",
    String -> IO (TrackedErrors ())
checkParseFail String
"",

    String -> GeneralInstance -> IO (TrackedErrors ())
checkParseSuccess
      String
"[Type0&Type0]"
      (forall a. (Eq a, Ord a) => a -> GeneralType a
singleType forall a b. (a -> b) -> a -> b
$ TypeInstance -> TypeInstanceOrParam
JustTypeInstance forall a b. (a -> b) -> a -> b
$ CategoryName -> InstanceParams -> TypeInstance
TypeInstance (String -> CategoryName
CategoryName String
"Type0") (forall a. [a] -> Positional a
Positional [])),
    String -> GeneralInstance -> IO (TrackedErrors ())
checkParseSuccess
      String
"[Type0|Type0]"
      (forall a. (Eq a, Ord a) => a -> GeneralType a
singleType forall a b. (a -> b) -> a -> b
$ TypeInstance -> TypeInstanceOrParam
JustTypeInstance forall a b. (a -> b) -> a -> b
$ CategoryName -> InstanceParams -> TypeInstance
TypeInstance (String -> CategoryName
CategoryName String
"Type0") (forall a. [a] -> Positional a
Positional [])),
    String -> GeneralInstance -> IO (TrackedErrors ())
checkParseSuccess String
"all" forall a. Bounded a => a
minBound,
    String -> GeneralInstance -> IO (TrackedErrors ())
checkParseSuccess String
"any" forall a. Bounded a => a
maxBound,
    String -> IO (TrackedErrors ())
checkParseFail String
"[Type0]",
    String -> IO (TrackedErrors ())
checkParseFail String
"[]",

    String -> GeneralInstance -> IO (TrackedErrors ())
checkParseSuccess
      String
"[Type1&Type0&Type1]"
      (forall a (f :: * -> *). (Mergeable a, Foldable f) => f a -> a
mergeAll [
          forall a. (Eq a, Ord a) => a -> GeneralType a
singleType forall a b. (a -> b) -> a -> b
$ TypeInstance -> TypeInstanceOrParam
JustTypeInstance forall a b. (a -> b) -> a -> b
$ CategoryName -> InstanceParams -> TypeInstance
TypeInstance (String -> CategoryName
CategoryName String
"Type0") (forall a. [a] -> Positional a
Positional []),
          forall a. (Eq a, Ord a) => a -> GeneralType a
singleType forall a b. (a -> b) -> a -> b
$ TypeInstance -> TypeInstanceOrParam
JustTypeInstance forall a b. (a -> b) -> a -> b
$ CategoryName -> InstanceParams -> TypeInstance
TypeInstance (String -> CategoryName
CategoryName String
"Type1") (forall a. [a] -> Positional a
Positional [])
        ]),
    String -> GeneralInstance -> IO (TrackedErrors ())
checkParseSuccess
      String
"[Type1|Type0|Type1]"
      (forall a (f :: * -> *). (Mergeable a, Foldable f) => f a -> a
mergeAny [
          forall a. (Eq a, Ord a) => a -> GeneralType a
singleType forall a b. (a -> b) -> a -> b
$ TypeInstance -> TypeInstanceOrParam
JustTypeInstance forall a b. (a -> b) -> a -> b
$ CategoryName -> InstanceParams -> TypeInstance
TypeInstance (String -> CategoryName
CategoryName String
"Type0") (forall a. [a] -> Positional a
Positional []),
          forall a. (Eq a, Ord a) => a -> GeneralType a
singleType forall a b. (a -> b) -> a -> b
$ TypeInstance -> TypeInstanceOrParam
JustTypeInstance forall a b. (a -> b) -> a -> b
$ CategoryName -> InstanceParams -> TypeInstance
TypeInstance (String -> CategoryName
CategoryName String
"Type1") (forall a. [a] -> Positional a
Positional [])
        ]),
    String -> IO (TrackedErrors ())
checkParseFail String
"[Type0&Type1|Type2]",
    String -> GeneralInstance -> IO (TrackedErrors ())
checkParseSuccess
      String
"[Type0<#x>&#x]"
      (forall a (f :: * -> *). (Mergeable a, Foldable f) => f a -> a
mergeAll [
          forall a. (Eq a, Ord a) => a -> GeneralType a
singleType forall a b. (a -> b) -> a -> b
$ TypeInstance -> TypeInstanceOrParam
JustTypeInstance forall a b. (a -> b) -> a -> b
$ CategoryName -> InstanceParams -> TypeInstance
TypeInstance (String -> CategoryName
CategoryName String
"Type0") (forall a. [a] -> Positional a
Positional [
              forall a. (Eq a, Ord a) => a -> GeneralType a
singleType forall a b. (a -> b) -> a -> b
$ Bool -> ParamName -> TypeInstanceOrParam
JustParamName Bool
False forall a b. (a -> b) -> a -> b
$ String -> ParamName
ParamName String
"#x"
            ]),
          forall a. (Eq a, Ord a) => a -> GeneralType a
singleType forall a b. (a -> b) -> a -> b
$ Bool -> ParamName -> TypeInstanceOrParam
JustParamName Bool
False forall a b. (a -> b) -> a -> b
$ String -> ParamName
ParamName String
"#x"
        ]),
    String -> IO (TrackedErrors ())
checkParseFail String
"[Type0&]",
    String -> IO (TrackedErrors ())
checkParseFail String
"[Type0|]",
    String -> IO (TrackedErrors ())
checkParseFail String
"[Type0 Type1]",

    String -> GeneralInstance -> IO (TrackedErrors ())
checkParseSuccess
      String
"[Type0&[Type1&Type3]&Type2]"
      (forall a (f :: * -> *). (Mergeable a, Foldable f) => f a -> a
mergeAll [
          forall a. (Eq a, Ord a) => a -> GeneralType a
singleType forall a b. (a -> b) -> a -> b
$ TypeInstance -> TypeInstanceOrParam
JustTypeInstance forall a b. (a -> b) -> a -> b
$ CategoryName -> InstanceParams -> TypeInstance
TypeInstance (String -> CategoryName
CategoryName String
"Type0") (forall a. [a] -> Positional a
Positional []),
          forall a. (Eq a, Ord a) => a -> GeneralType a
singleType forall a b. (a -> b) -> a -> b
$ TypeInstance -> TypeInstanceOrParam
JustTypeInstance forall a b. (a -> b) -> a -> b
$ CategoryName -> InstanceParams -> TypeInstance
TypeInstance (String -> CategoryName
CategoryName String
"Type1") (forall a. [a] -> Positional a
Positional []),
          forall a. (Eq a, Ord a) => a -> GeneralType a
singleType forall a b. (a -> b) -> a -> b
$ TypeInstance -> TypeInstanceOrParam
JustTypeInstance forall a b. (a -> b) -> a -> b
$ CategoryName -> InstanceParams -> TypeInstance
TypeInstance (String -> CategoryName
CategoryName String
"Type2") (forall a. [a] -> Positional a
Positional []),
          forall a. (Eq a, Ord a) => a -> GeneralType a
singleType forall a b. (a -> b) -> a -> b
$ TypeInstance -> TypeInstanceOrParam
JustTypeInstance forall a b. (a -> b) -> a -> b
$ CategoryName -> InstanceParams -> TypeInstance
TypeInstance (String -> CategoryName
CategoryName String
"Type3") (forall a. [a] -> Positional a
Positional [])
        ]),
    String -> GeneralInstance -> IO (TrackedErrors ())
checkParseSuccess
      String
"[Type0|[Type1|Type3]|Type2]"
      (forall a (f :: * -> *). (Mergeable a, Foldable f) => f a -> a
mergeAny [
          forall a. (Eq a, Ord a) => a -> GeneralType a
singleType forall a b. (a -> b) -> a -> b
$ TypeInstance -> TypeInstanceOrParam
JustTypeInstance forall a b. (a -> b) -> a -> b
$ CategoryName -> InstanceParams -> TypeInstance
TypeInstance (String -> CategoryName
CategoryName String
"Type0") (forall a. [a] -> Positional a
Positional []),
          forall a. (Eq a, Ord a) => a -> GeneralType a
singleType forall a b. (a -> b) -> a -> b
$ TypeInstance -> TypeInstanceOrParam
JustTypeInstance forall a b. (a -> b) -> a -> b
$ CategoryName -> InstanceParams -> TypeInstance
TypeInstance (String -> CategoryName
CategoryName String
"Type1") (forall a. [a] -> Positional a
Positional []),
          forall a. (Eq a, Ord a) => a -> GeneralType a
singleType forall a b. (a -> b) -> a -> b
$ TypeInstance -> TypeInstanceOrParam
JustTypeInstance forall a b. (a -> b) -> a -> b
$ CategoryName -> InstanceParams -> TypeInstance
TypeInstance (String -> CategoryName
CategoryName String
"Type2") (forall a. [a] -> Positional a
Positional []),
          forall a. (Eq a, Ord a) => a -> GeneralType a
singleType forall a b. (a -> b) -> a -> b
$ TypeInstance -> TypeInstanceOrParam
JustTypeInstance forall a b. (a -> b) -> a -> b
$ CategoryName -> InstanceParams -> TypeInstance
TypeInstance (String -> CategoryName
CategoryName String
"Type3") (forall a. [a] -> Positional a
Positional [])
        ]),
    String -> GeneralInstance -> IO (TrackedErrors ())
checkParseSuccess
      String
"[Type0&[Type1|Type3]&Type2]"
      (forall a (f :: * -> *). (Mergeable a, Foldable f) => f a -> a
mergeAll [
          forall a. (Eq a, Ord a) => a -> GeneralType a
singleType forall a b. (a -> b) -> a -> b
$ TypeInstance -> TypeInstanceOrParam
JustTypeInstance forall a b. (a -> b) -> a -> b
$ CategoryName -> InstanceParams -> TypeInstance
TypeInstance (String -> CategoryName
CategoryName String
"Type0") (forall a. [a] -> Positional a
Positional []),
          forall a. (Eq a, Ord a) => a -> GeneralType a
singleType forall a b. (a -> b) -> a -> b
$ TypeInstance -> TypeInstanceOrParam
JustTypeInstance forall a b. (a -> b) -> a -> b
$ CategoryName -> InstanceParams -> TypeInstance
TypeInstance (String -> CategoryName
CategoryName String
"Type2") (forall a. [a] -> Positional a
Positional []),
          forall a (f :: * -> *). (Mergeable a, Foldable f) => f a -> a
mergeAny [
              forall a. (Eq a, Ord a) => a -> GeneralType a
singleType forall a b. (a -> b) -> a -> b
$ TypeInstance -> TypeInstanceOrParam
JustTypeInstance forall a b. (a -> b) -> a -> b
$ CategoryName -> InstanceParams -> TypeInstance
TypeInstance (String -> CategoryName
CategoryName String
"Type1") (forall a. [a] -> Positional a
Positional []),
              forall a. (Eq a, Ord a) => a -> GeneralType a
singleType forall a b. (a -> b) -> a -> b
$ TypeInstance -> TypeInstanceOrParam
JustTypeInstance forall a b. (a -> b) -> a -> b
$ CategoryName -> InstanceParams -> TypeInstance
TypeInstance (String -> CategoryName
CategoryName String
"Type3") (forall a. [a] -> Positional a
Positional [])
            ]
        ]),
    String -> GeneralInstance -> IO (TrackedErrors ())
checkParseSuccess
      String
"[Type0|[Type1&Type3]|Type2]"
      (forall a (f :: * -> *). (Mergeable a, Foldable f) => f a -> a
mergeAny [
          forall a. (Eq a, Ord a) => a -> GeneralType a
singleType forall a b. (a -> b) -> a -> b
$ TypeInstance -> TypeInstanceOrParam
JustTypeInstance forall a b. (a -> b) -> a -> b
$ CategoryName -> InstanceParams -> TypeInstance
TypeInstance (String -> CategoryName
CategoryName String
"Type0") (forall a. [a] -> Positional a
Positional []),
          forall a. (Eq a, Ord a) => a -> GeneralType a
singleType forall a b. (a -> b) -> a -> b
$ TypeInstance -> TypeInstanceOrParam
JustTypeInstance forall a b. (a -> b) -> a -> b
$ CategoryName -> InstanceParams -> TypeInstance
TypeInstance (String -> CategoryName
CategoryName String
"Type2") (forall a. [a] -> Positional a
Positional []),
          forall a (f :: * -> *). (Mergeable a, Foldable f) => f a -> a
mergeAll [
              forall a. (Eq a, Ord a) => a -> GeneralType a
singleType forall a b. (a -> b) -> a -> b
$ TypeInstance -> TypeInstanceOrParam
JustTypeInstance forall a b. (a -> b) -> a -> b
$ CategoryName -> InstanceParams -> TypeInstance
TypeInstance (String -> CategoryName
CategoryName String
"Type1") (forall a. [a] -> Positional a
Positional []),
              forall a. (Eq a, Ord a) => a -> GeneralType a
singleType forall a b. (a -> b) -> a -> b
$ TypeInstance -> TypeInstanceOrParam
JustTypeInstance forall a b. (a -> b) -> a -> b
$ CategoryName -> InstanceParams -> TypeInstance
TypeInstance (String -> CategoryName
CategoryName String
"Type3") (forall a. [a] -> Positional a
Positional [])
            ]
        ]),

    String -> String -> IO (TrackedErrors ())
checkSimpleConvertSuccess
      String
"Type0"
      String
"Type0",
    String -> String -> IO (TrackedErrors ())
checkSimpleConvertSuccess
      String
"Type3"
      String
"Type0",
    String -> String -> IO (TrackedErrors ())
checkSimpleConvertFail
      String
"Type0"
      String
"Type3",
    String -> String -> IO (TrackedErrors ())
checkSimpleConvertSuccess
      String
"Type1<Type0>"
      String
"Type0",
    String -> String -> IO (TrackedErrors ())
checkSimpleConvertFail
      String
"Type0"
      String
"Type1<Type0>",
    String -> String -> IO (TrackedErrors ())
checkSimpleConvertSuccess
      String
"Type2<Type0,Type0,Type0>"
      String
"Type2<Type0,Type0,Type0>",
    String -> String -> IO (TrackedErrors ())
checkSimpleConvertSuccess
      String
"Type2<Type0,Type0,Type3>"
      String
"Type2<Type3,Type0,Type0>",
    String -> String -> IO (TrackedErrors ())
checkSimpleConvertFail
      String
"Type2<Type3,Type0,Type3>"
      String
"Type2<Type0,Type0,Type0>",
    String -> String -> IO (TrackedErrors ())
checkSimpleConvertFail
      String
"Type2<Type0,Type0,Type0>"
      String
"Type2<Type3,Type0,Type3>",
    String -> String -> IO (TrackedErrors ())
checkSimpleConvertFail
      String
"Type2<Type0,Type3,Type0>"
      String
"Type2<Type0,Type0,Type0>",
    String -> String -> IO (TrackedErrors ())
checkSimpleConvertFail
      String
"Type2<Type0,Type0,Type0>"
      String
"Type2<Type0,Type3,Type0>",
    String -> String -> IO (TrackedErrors ())
checkSimpleConvertSuccess
      String
"Type3"
      String
"[Type0|Type3]",
    String -> String -> IO (TrackedErrors ())
checkSimpleConvertSuccess
      String
"Type3"
      String
"[Type0|Type1<Type0>]",
    String -> String -> IO (TrackedErrors ())
checkSimpleConvertSuccess
      String
"[Type3|Type1<Type0>]"
      String
"Type0",
    String -> String -> IO (TrackedErrors ())
checkSimpleConvertSuccess
      String
"[Type0&Type3]"
      String
"Type3",
    String -> String -> IO (TrackedErrors ())
checkSimpleConvertSuccess
      String
"[Type3|Type3]"
      String
"Type3",
    String -> String -> IO (TrackedErrors ())
checkSimpleConvertSuccess
      String
"[Type1<Type0>&Type3]"
      String
"[Type1<Type0>|Type3]",
    String -> String -> IO (TrackedErrors ())
checkSimpleConvertFail
      String
"[Type0|Type3]"
      String
"Type3",
    String -> String -> IO (TrackedErrors ())
checkSimpleConvertFail
      String
"Type0"
      String
"[Type0&Type3]",
    String -> String -> IO (TrackedErrors ())
checkSimpleConvertFail
      String
"[Type0|Type3]"
      String
"[Type0&Type3]",

    -- Make sure that both sides are separately expanded with checks from
    -- intersection to union.
    String -> String -> IO (TrackedErrors ())
checkSimpleConvertSuccess
      String
"[Type1<Type0>&Type4<Type0>]"
      String
"[[Type1<Type0>&Type4<Type0>]|Type5<Type0>]",
    String -> String -> IO (TrackedErrors ())
checkSimpleConvertSuccess
      String
"[[Type1<Type0>|Type4<Type0>]&Type5<Type0>]"
      String
"[Type1<Type0>|Type4<Type0>]",

    String -> String -> IO (TrackedErrors ())
checkSimpleConvertSuccess
      String
"any"
      String
"any",
    String -> String -> IO (TrackedErrors ())
checkSimpleConvertSuccess
      String
"Type0"
      String
"any",
    String -> String -> IO (TrackedErrors ())
checkSimpleConvertFail
      String
"any"
      String
"Type0",
    String -> String -> IO (TrackedErrors ())
checkSimpleConvertSuccess
      String
"all"
      String
"all",
    String -> String -> IO (TrackedErrors ())
checkSimpleConvertFail
      String
"Type0"
      String
"all",
    String -> String -> IO (TrackedErrors ())
checkSimpleConvertSuccess
      String
"all"
      String
"Type0",
    String -> String -> IO (TrackedErrors ())
checkSimpleConvertSuccess
      String
"all"
      String
"any",
    String -> String -> IO (TrackedErrors ())
checkSimpleConvertFail
      String
"any"
      String
"all",
    String -> String -> IO (TrackedErrors ())
checkSimpleConvertFail
      String
"Type1<Type0>"
      String
"Type1<any>",
    String -> String -> IO (TrackedErrors ())
checkSimpleConvertFail
      String
"Type1<all>"
      String
"Type1<Type0>",
    String -> String -> IO (TrackedErrors ())
checkSimpleConvertFail
      String
"Type1<all>"
      String
"Type1<any>",
    String -> String -> IO (TrackedErrors ())
checkSimpleConvertFail
      String
"Type1<any>"
      String
"Type1<all>",
    String -> String -> IO (TrackedErrors ())
checkSimpleConvertSuccess
      String
"Type1<any>"
      String
"Type1<any>",
    String -> String -> IO (TrackedErrors ())
checkSimpleConvertSuccess
      String
"Type1<all>"
      String
"Type1<all>",

    [(String, [String])] -> String -> String -> IO (TrackedErrors ())
checkConvertSuccess
      [(String
"#x",[])]
      String
"#x" String
"#x",
    [(String, [String])] -> String -> String -> IO (TrackedErrors ())
checkConvertFail
      [(String
"#x",[]),
       (String
"#y",[])]
      String
"#x" String
"#y",
    [(String, [String])] -> String -> String -> IO (TrackedErrors ())
checkConvertSuccess
      [(String
"#x",[String
"requires #y"]),
       (String
"#y",[String
"allows #x"])]
      String
"#x" String
"#y",
    [(String, [String])] -> String -> String -> IO (TrackedErrors ())
checkConvertSuccess
      [(String
"#x",[String
"requires #y"]),
       (String
"#y",[])]
      String
"#x" String
"#y",
    [(String, [String])] -> String -> String -> IO (TrackedErrors ())
checkConvertSuccess
      [(String
"#x",[]),
       (String
"#y",[String
"allows #x"])]
      String
"#x" String
"#y",

    -- NOTE: defines are not checked for instance conversions.
    [(String, [String])] -> String -> String -> IO (TrackedErrors ())
checkConvertSuccess
      [(String
"#x",[String
"requires #y",String
"defines Instance0"]),
       (String
"#y",[String
"allows #x"])]
      String
"#x" String
"#y",
    [(String, [String])] -> String -> String -> IO (TrackedErrors ())
checkConvertSuccess
      [(String
"#x",[String
"requires #y"]),
       (String
"#y",[String
"allows #x",String
"defines Instance0"])]
      String
"#x" String
"#y",
    [(String, [String])] -> String -> String -> IO (TrackedErrors ())
checkConvertSuccess
      [(String
"#x",[String
"requires #y",String
"defines Instance0"]),
       (String
"#y",[String
"allows #x",String
"defines Instance0"])]
      String
"#x" String
"#y",
    [(String, [String])] -> String -> String -> IO (TrackedErrors ())
checkConvertFail
      [(String
"#x",[String
"defines Instance0"]),
       (String
"#y",[String
"defines Instance0"])]
      String
"#x" String
"#y",
    [(String, [String])] -> String -> String -> IO (TrackedErrors ())
checkConvertSuccess
      [(String
"#x",[String
"requires Type0",String
"defines Instance0"])]
      String
"#x" String
"Type0",
    [(String, [String])] -> String -> String -> IO (TrackedErrors ())
checkConvertSuccess
      [(String
"#x",[String
"allows Type0",String
"defines Instance0"])]
      String
"Type0" String
"#x",

    [(String, [String])] -> String -> String -> IO (TrackedErrors ())
checkConvertSuccess
      [(String
"#x",[String
"requires #z"]),
       (String
"#y",[String
"allows #z"]),
       (String
"#z",[])]
      String
"#x" String
"#y",
    [(String, [String])] -> String -> String -> IO (TrackedErrors ())
checkConvertSuccess
      [(String
"#x",[String
"requires #z"]),
       (String
"#y",[]),
       (String
"#z",[String
"requires #y"])]
      String
"#x" String
"#y",
    -- NOTE: This is technically valid, but the checking mechanism doesn't do
    -- a full graph search, so the writer needs to be explicit about implied
    -- additional filters, e.g., "#x requires #y" => "#y allows #x".
    [(String, [String])] -> String -> String -> IO (TrackedErrors ())
checkConvertFail
      [(String
"#w",[String
"allows #x"]),
       (String
"#x",[]),
       (String
"#y",[]),
       (String
"#z",[String
"allows #w",String
"requires #y"])]
      String
"#x" String
"#y",
    [(String, [String])] -> String -> String -> IO (TrackedErrors ())
checkConvertSuccess
      [(String
"#x",[String
"requires Type3"]),
       (String
"#y",[String
"allows Type0"])]
      String
"#x" String
"#y",
    [(String, [String])] -> String -> String -> IO (TrackedErrors ())
checkConvertSuccess
      [(String
"#x",[String
"requires #y"]),
       (String
"#y",[String
"requires Type3"])]
      String
"#x" String
"Type0",
    [(String, [String])] -> String -> String -> IO (TrackedErrors ())
checkConvertSuccess
      [(String
"#x",[String
"allows #y"]),
       (String
"#y",[String
"allows Type0"])]
      String
"Type3" String
"#x",

    [(String, [String])] -> String -> String -> IO (TrackedErrors ())
checkConvertSuccess
      [(String
"#x",[])]
      String
"Type2<Type0,Type0,#x>" String
"Type2<Type0,Type0,#x>",
    [(String, [String])] -> String -> String -> IO (TrackedErrors ())
checkConvertFail
      [(String
"#x",[]),
       (String
"#y",[])]
      String
"Type2<Type0,Type0,#x>" String
"Type2<Type0,Type0,#y>",
    [(String, [String])] -> String -> String -> IO (TrackedErrors ())
checkConvertSuccess
      [(String
"#x",[String
"requires #y"]),
       (String
"#y",[String
"allows #x"])]
      String
"Type2<Type0,Type0,#x>" String
"Type2<Type0,Type0,#y>",
    [(String, [String])] -> String -> String -> IO (TrackedErrors ())
checkConvertSuccess
      [(String
"#x",[String
"requires #y"]),
       (String
"#y",[])]
      String
"Type2<Type0,Type0,#x>" String
"Type2<Type0,Type0,#y>",
    [(String, [String])] -> String -> String -> IO (TrackedErrors ())
checkConvertSuccess
      [(String
"#x",[]),
       (String
"#y",[String
"allows #x"])]
      String
"Type2<Type0,Type0,#x>" String
"Type2<Type0,Type0,#y>",

    [(String, [String])] -> String -> String -> IO (TrackedErrors ())
checkConvertSuccess
      [(String
"#x",[])]
      String
"Type2<#x,Type0,Type0>" String
"Type2<#x,Type0,Type0>",
    [(String, [String])] -> String -> String -> IO (TrackedErrors ())
checkConvertFail
      [(String
"#x",[]),
       (String
"#y",[])]
      String
"Type2<#x,Type0,Type0>" String
"Type2<#y,Type0,Type0>",
    [(String, [String])] -> String -> String -> IO (TrackedErrors ())
checkConvertFail
      [(String
"#x",[String
"requires #y"]),
       (String
"#y",[String
"allows #x"])]
      String
"Type2<#x,Type0,Type0>" String
"Type2<#y,Type0,Type0>",
    [(String, [String])] -> String -> String -> IO (TrackedErrors ())
checkConvertFail
      [(String
"#x",[String
"requires #y"]),
       (String
"#y",[])]
      String
"Type2<#x,Type0,Type0>" String
"Type2<#y,Type0,Type0>",
    [(String, [String])] -> String -> String -> IO (TrackedErrors ())
checkConvertFail
      [(String
"#x",[]),
       (String
"#y",[String
"allows #x"])]
      String
"Type2<#x,Type0,Type0>" String
"Type2<#y,Type0,Type0>",
    [(String, [String])] -> String -> String -> IO (TrackedErrors ())
checkConvertSuccess
      [(String
"#x",[String
"allows #y"]),
       (String
"#y",[String
"requires #x"])]
      String
"Type2<#x,Type0,Type0>" String
"Type2<#y,Type0,Type0>",
    [(String, [String])] -> String -> String -> IO (TrackedErrors ())
checkConvertSuccess
      [(String
"#x",[String
"allows #y"]),
       (String
"#y",[])]
      String
"Type2<#x,Type0,Type0>" String
"Type2<#y,Type0,Type0>",
    [(String, [String])] -> String -> String -> IO (TrackedErrors ())
checkConvertSuccess
      [(String
"#x",[]),
       (String
"#y",[String
"requires #x"])]
      String
"Type2<#x,Type0,Type0>" String
"Type2<#y,Type0,Type0>",

    [(String, [String])] -> String -> String -> IO (TrackedErrors ())
checkConvertFail
      [(String
"#x",[])]
      String
"#x" String
"Type0",
    [(String, [String])] -> String -> String -> IO (TrackedErrors ())
checkConvertSuccess
      [(String
"#x",[String
"requires Type0"])]
      String
"#x" String
"Type0",
    [(String, [String])] -> String -> String -> IO (TrackedErrors ())
checkConvertSuccess
      [(String
"#x",[String
"requires Type3"])]
      String
"#x" String
"Type0",
    [(String, [String])] -> String -> String -> IO (TrackedErrors ())
checkConvertFail
      [(String
"#x",[])]
      String
"Type0" String
"#x",
    [(String, [String])] -> String -> String -> IO (TrackedErrors ())
checkConvertSuccess
      [(String
"#x",[String
"allows Type0"])]
      String
"Type0" String
"#x",
    [(String, [String])] -> String -> String -> IO (TrackedErrors ())
checkConvertSuccess
      [(String
"#x",[String
"allows Type0"])]
      String
"Type3" String
"#x",

    [(String, [String])] -> String -> String -> IO (TrackedErrors ())
checkConvertFail
      [(String
"#x",[])]
      String
"Type2<#x,Type0,Type0>" String
"Type2<Type0,Type0,Type0>",
    [(String, [String])] -> String -> String -> IO (TrackedErrors ())
checkConvertSuccess
      [(String
"#x",[String
"allows Type0"])]
      String
"Type2<#x,Type0,Type0>" String
"Type2<Type0,Type0,Type0>",
    [(String, [String])] -> String -> String -> IO (TrackedErrors ())
checkConvertSuccess
      [(String
"#x",[String
"allows Type0"])]
      String
"Type2<#x,Type0,Type0>" String
"Type2<Type3,Type0,Type0>",
    [(String, [String])] -> String -> String -> IO (TrackedErrors ())
checkConvertFail
      [(String
"#x",[])]
      String
"Type2<Type0,Type0,Type0>" String
"Type2<#x,Type0,Type0>",
    [(String, [String])] -> String -> String -> IO (TrackedErrors ())
checkConvertSuccess
      [(String
"#x",[String
"requires Type0"])]
      String
"Type2<Type0,Type0,Type0>" String
"Type2<#x,Type0,Type0>",
    [(String, [String])] -> String -> String -> IO (TrackedErrors ())
checkConvertSuccess
      [(String
"#x",[String
"requires Type3"])]
      String
"Type2<Type0,Type0,Type0>" String
"Type2<#x,Type0,Type0>",

    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall r.
TypeResolver r =>
r -> [String] -> String -> TrackedErrors ()
checkTypeSuccess Resolver
Resolver
      []
      String
"Type4<Type0>",
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall r.
TypeResolver r =>
r -> [String] -> String -> TrackedErrors ()
checkTypeSuccess Resolver
Resolver
      [String
"#x"]
      String
"Type4<[#x&Type0]>",
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall r.
TypeResolver r =>
r -> [String] -> String -> TrackedErrors ()
checkTypeSuccess Resolver
Resolver
      [String
"#x"]
      String
"Type4<[#x|Type0]>",
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall r.
TypeResolver r =>
r -> [String] -> String -> TrackedErrors ()
checkTypeSuccess Resolver
Resolver
      [String
"#x"]
      String
"Type4<[#x|Type3]>",
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall r.
TypeResolver r =>
r -> [String] -> String -> TrackedErrors ()
checkTypeFail Resolver
Resolver
      []
      String
"Type5<#x>",
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall r.
TypeResolver r =>
r -> [String] -> String -> TrackedErrors ()
checkTypeSuccess Resolver
Resolver
      [String
"#x"]
      String
"Type5<#x>",

    [(String, [String])] -> String -> String -> IO (TrackedErrors ())
checkConvertSuccess
      [(String
"#x",[String
"requires #y"]),
       (String
"#y",[String
"requires #z"]),
       (String
"#z",[])]
      String
"#x" String
"#y",
    [(String, [String])] -> String -> String -> IO (TrackedErrors ())
checkConvertSuccess
      [(String
"#x",[String
"allows #z"]),
       (String
"#y",[String
"allows #x"]),
       (String
"#z",[])]
      String
"#x" String
"#y",

    String -> String -> IO (TrackedErrors ())
checkSimpleConvertSuccess
      String
"any"
      String
"any",
    String -> String -> IO (TrackedErrors ())
checkSimpleConvertSuccess
      String
"all"
      String
"all",
    String -> String -> IO (TrackedErrors ())
checkSimpleConvertSuccess
      String
"all"
      String
"any",
    [(String, [String])] -> String -> String -> IO (TrackedErrors ())
checkConvertSuccess
      [(String
"#x",[]),
       (String
"#y",[])]
      String
"[#x&#y]" String
"[#x&#y]",
    [(String, [String])] -> String -> String -> IO (TrackedErrors ())
checkConvertSuccess
      [(String
"#x",[]),
       (String
"#y",[])]
      String
"[#x&#y]" String
"[#x|#y]",
    [(String, [String])] -> String -> String -> IO (TrackedErrors ())
checkConvertSuccess
      [(String
"#x",[]),
       (String
"#y",[])]
      String
"[#x|#y]" String
"[#x|#y]",
    [(String, [String])] -> String -> String -> IO (TrackedErrors ())
checkConvertSuccess
      [(String
"#x",[]),
       (String
"#y",[String
"defines Instance0"])]
      String
"[#x&#y]" String
"[#x|#y]",
    [(String, [String])] -> String -> String -> IO (TrackedErrors ())
checkConvertSuccess
      [(String
"#x",[]),
       (String
"#y",[String
"defines Instance0"])]
      String
"[#x&#y]" String
"#y",
    [(String, [String])] -> String -> String -> IO (TrackedErrors ())
checkConvertFail
      [(String
"#x",[]),
       (String
"#y",[String
"defines Instance0"])]
      String
"[#x|#y]" String
"#y",
    [(String, [String])] -> String -> String -> IO (TrackedErrors ())
checkConvertSuccess
      [(String
"#x",[]),
       (String
"#y",[String
"requires Type3"])]
      String
"[#x&#y]" String
"[#x|#y]",
    [(String, [String])] -> String -> String -> IO (TrackedErrors ())
checkConvertSuccess
      [(String
"#x",[]),
       (String
"#y",[String
"requires Type3"])]
      String
"[#x&#y]" String
"#y",
    [(String, [String])] -> String -> String -> IO (TrackedErrors ())
checkConvertFail
      [(String
"#x",[]),
       (String
"#y",[String
"requires Type3"])]
      String
"[#x|#y]" String
"#y",
    [(String, [String])] -> String -> String -> IO (TrackedErrors ())
checkConvertSuccess
      [(String
"#x",[])]
      String
"all" String
"#x",
    [(String, [String])] -> String -> String -> IO (TrackedErrors ())
checkConvertSuccess
      [(String
"#x",[String
"defines Instance0"])]
      String
"all" String
"#x",
    [(String, [String])] -> String -> String -> IO (TrackedErrors ())
checkConvertSuccess
      [(String
"#x",[String
"requires Type3"])]
      String
"all" String
"#x",

    String -> String -> IO (TrackedErrors ())
checkSimpleConvertSuccess
      String
"optional Type0"
      String
"optional Type0",
    String -> String -> IO (TrackedErrors ())
checkSimpleConvertSuccess
      String
"weak Type0"
      String
"weak Type0",
    String -> String -> IO (TrackedErrors ())
checkSimpleConvertSuccess
      String
"Type0"
      String
"optional Type0",
    String -> String -> IO (TrackedErrors ())
checkSimpleConvertSuccess
      String
"Type0"
      String
"weak Type0",
    String -> String -> IO (TrackedErrors ())
checkSimpleConvertSuccess
      String
"optional Type0"
      String
"weak Type0",
    String -> String -> IO (TrackedErrors ())
checkSimpleConvertFail
      String
"optional Type0"
      String
"Type0",
    String -> String -> IO (TrackedErrors ())
checkSimpleConvertFail
      String
"weak Type0"
      String
"Type0",
    String -> String -> IO (TrackedErrors ())
checkSimpleConvertFail
      String
"weak Type0"
      String
"optional Type0",

    String -> String -> IO (TrackedErrors ())
checkSimpleConvertSuccess
      String
"optional Type3"
      String
"optional Type0",
    String -> String -> IO (TrackedErrors ())
checkSimpleConvertSuccess
      String
"weak Type3"
      String
"weak Type0",
    String -> String -> IO (TrackedErrors ())
checkSimpleConvertSuccess
      String
"Type3"
      String
"optional Type0",
    String -> String -> IO (TrackedErrors ())
checkSimpleConvertSuccess
      String
"Type3"
      String
"weak Type0",
    String -> String -> IO (TrackedErrors ())
checkSimpleConvertSuccess
      String
"optional Type3"
      String
"weak Type0",

    String -> String -> IO (TrackedErrors ())
checkSimpleConvertSuccess
      String
"any"
      String
"optional any",
    String -> String -> IO (TrackedErrors ())
checkSimpleConvertSuccess
      String
"Type3"
      String
"optional any",
    String -> String -> IO (TrackedErrors ())
checkSimpleConvertSuccess
      String
"optional all"
      String
"optional Type3",

    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall r.
TypeResolver r =>
r -> [String] -> String -> TrackedErrors ()
checkTypeSuccess Resolver
Resolver
      [String
"#x"]
      String
"#x",
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall r.
TypeResolver r =>
r -> [String] -> String -> TrackedErrors ()
checkTypeSuccess Resolver
Resolver
      [String
"#x"]
      String
"Type1<#x>",
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall r.
TypeResolver r =>
r -> [String] -> String -> TrackedErrors ()
checkTypeSuccess Resolver
Resolver
      []
      String
"Type1<all>",
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall r.
TypeResolver r =>
r -> [String] -> String -> TrackedErrors ()
checkTypeSuccess Resolver
Resolver
      [String
"#x"]
      String
"Type1<#x>",
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall r.
TypeResolver r =>
r -> [String] -> String -> TrackedErrors ()
checkTypeSuccess Resolver
Resolver
      []
      String
"Type1<Type3>",
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall r.
TypeResolver r =>
r -> [String] -> String -> TrackedErrors ()
checkTypeSuccess Resolver
Resolver
      []
      String
"Type1<Type1<Type3>>",
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall r.
TypeResolver r =>
r -> [String] -> String -> TrackedErrors ()
checkTypeSuccess Resolver
Resolver
      []
      String
"Type2<Type0,Type0,Type0>",
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall r.
TypeResolver r =>
r -> [String] -> String -> TrackedErrors ()
checkTypeSuccess Resolver
Resolver
      []
      String
"Type2<all,Type0,Type0>",
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall r.
TypeResolver r =>
r -> [String] -> String -> TrackedErrors ()
checkTypeSuccess Resolver
Resolver
      []
      String
"Type2<any,Type0,Type0>",
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall r.
TypeResolver r =>
r -> [String] -> String -> TrackedErrors ()
checkTypeSuccess Resolver
Resolver
      []
      String
"Type4<any>",
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall r.
TypeResolver r =>
r -> [String] -> String -> TrackedErrors ()
checkTypeSuccess Resolver
Resolver
      []
      String
"Type4<all>",

    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall r.
TypeResolver r =>
r -> [String] -> String -> TrackedErrors ()
checkTypeSuccess Resolver
Resolver
      [String
"#x"]
      String
"Type2<#x,#x,#x>",

    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall r.
TypeResolver r =>
r -> [String] -> String -> TrackedErrors ()
checkTypeSuccess Resolver
Resolver
      []
      String
"Type4<Type0>",
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall r.
TypeResolver r =>
r -> [String] -> String -> TrackedErrors ()
checkTypeFail Resolver
Resolver
      []
      String
"Type5<#x>",
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall r.
TypeResolver r =>
r -> [String] -> String -> TrackedErrors ()
checkTypeSuccess Resolver
Resolver
      [String
"#x"]
      String
"Type5<#x>",

    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall r.
TypeResolver r =>
r -> [String] -> String -> TrackedErrors ()
checkTypeSuccess Resolver
Resolver
      []
      String
"[Type4<Type0>|Type1<Type3>]",
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall r.
TypeResolver r =>
r -> [String] -> String -> TrackedErrors ()
checkTypeSuccess Resolver
Resolver
      []
      String
"[Type4<Type0>&Type1<Type3>]",
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall r.
TypeResolver r =>
r -> [String] -> String -> TrackedErrors ()
checkTypeSuccess Resolver
Resolver
      [String
"#x"]
      String
"[Type5<#x>|Type1<Type3>]",
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall r.
TypeResolver r =>
r -> [String] -> String -> TrackedErrors ()
checkTypeSuccess Resolver
Resolver
      [String
"#x"]
      String
"[Type5<#x>&Type1<Type3>]",
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall r.
TypeResolver r =>
r -> [String] -> String -> TrackedErrors ()
checkTypeSuccess Resolver
Resolver
      [String
"#x"]
      String
"[#x|Type1<Type3>]",
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall r.
TypeResolver r =>
r -> [String] -> String -> TrackedErrors ()
checkTypeSuccess Resolver
Resolver
      [String
"#x"]
      String
"[#x&Type1<Type3>]",
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall r.
TypeResolver r =>
r -> [String] -> String -> TrackedErrors ()
checkTypeFail Resolver
Resolver
      [String
"#x"]
      String
"[Type4<Type0>|Instance0]",
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall r.
TypeResolver r =>
r -> [String] -> String -> TrackedErrors ()
checkTypeFail Resolver
Resolver
      [String
"#x"]
      String
"[Type4<Type0>&Instance0]",

    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall r.
TypeResolver r =>
r -> [String] -> String -> TrackedErrors ()
checkTypeSuccess Resolver
Resolver
      []
      String
"[[Type4<Type0>&Type1<Type3>]|Type1<Type3>]",
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall r.
TypeResolver r =>
r -> [String] -> String -> TrackedErrors ()
checkTypeSuccess Resolver
Resolver
      []
      String
"[[Type4<Type0>|Type1<Type3>]&Type1<Type3>]",
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall r.
TypeResolver r =>
r -> [String] -> String -> TrackedErrors ()
checkTypeSuccess Resolver
Resolver
      [String
"#x"]
      String
"[[Type4<Type0>&#x]|Type1<Type3>]",
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall r.
TypeResolver r =>
r -> [String] -> String -> TrackedErrors ()
checkTypeSuccess Resolver
Resolver
      [String
"#x"]
      String
"[[Type4<Type0>|#x]&Type1<Type3>]",

    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall r.
TypeResolver r =>
r -> [String] -> String -> TrackedErrors ()
checkDefinesSuccess Resolver
Resolver
      [String
"#x"]
      String
"Instance1<#x>",
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall r.
TypeResolver r =>
r -> [String] -> String -> TrackedErrors ()
checkDefinesFail Resolver
Resolver
      []
      String
"Instance1<#x>",
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall r.
TypeResolver r =>
r -> [String] -> String -> TrackedErrors ()
checkDefinesSuccess Resolver
Resolver
      []
      String
"Instance1<Type3>",
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall r.
TypeResolver r =>
r -> [String] -> String -> TrackedErrors ()
checkDefinesSuccess Resolver
Resolver
      []
      String
"Instance1<Type1<Type3>>",

    [(String, [String])]
-> [String]
-> String
-> String
-> MergeTree (String, String, Variance)
-> IO (TrackedErrors ())
checkInferenceSuccess
      [(String
"#x",[])] [String
"#x"]
      String
"Type1<Type0>" String
"Type1<#x>"
      (forall a. a -> MergeTree a
mergeLeaf (String
"#x",String
"Type0",Variance
Invariant)),
    [(String, [String])]
-> [String] -> String -> String -> IO (TrackedErrors ())
checkInferenceFail
      [(String
"#x",[])] [String
"#x"]
      String
"Type1<Type3>" String
"Type4<#x>",

    [(String, [String])]
-> [String]
-> String
-> String
-> MergeTree (String, String, Variance)
-> IO (TrackedErrors ())
checkInferenceSuccess
      [(String
"#x",[])] [String
"#x"]
      -- Invariant should not be split for non-merged types.
      String
"Type1<Type1<Type1<Type0>>>" String
"Type1<Type1<Type1<#x>>>"
      (forall a. a -> MergeTree a
mergeLeaf (String
"#x",String
"Type0",Variance
Invariant)),

    [(String, [String])]
-> [String]
-> String
-> String
-> MergeTree (String, String, Variance)
-> IO (TrackedErrors ())
checkInferenceSuccess
      [(String
"#x",[])] [String
"#x"]
      String
"Instance1<Type1<Type3>>" String
"Instance1<#x>"
      (forall a. a -> MergeTree a
mergeLeaf (String
"#x",String
"Type1<Type3>",Variance
Contravariant)),
    [(String, [String])]
-> [String]
-> String
-> String
-> MergeTree (String, String, Variance)
-> IO (TrackedErrors ())
checkInferenceSuccess
      [(String
"#x",[])] [String
"#x"]
      String
"Instance1<Type1<Type3>>" String
"Instance1<Type1<#x>>"
      (forall a. a -> MergeTree a
mergeLeaf (String
"#x",String
"Type3",Variance
Invariant)),

    [(String, [String])]
-> [String]
-> String
-> String
-> MergeTree (String, String, Variance)
-> IO (TrackedErrors ())
checkInferenceSuccess
      [(String
"#x",[])] [String
"#x"]
      String
"Type2<Type3,Type0,Type3>" String
"Type2<#x,Type0,#x>"
      (forall a (f :: * -> *). (Mergeable a, Foldable f) => f a -> a
mergeAll [forall a. a -> MergeTree a
mergeLeaf (String
"#x",String
"Type3",Variance
Contravariant),
                 forall a. a -> MergeTree a
mergeLeaf (String
"#x",String
"Type3",Variance
Covariant)]),
    [(String, [String])]
-> [String]
-> String
-> String
-> MergeTree (String, String, Variance)
-> IO (TrackedErrors ())
checkInferenceSuccess
      [(String
"#x",[]),(String
"#y",[])] [String
"#x"]
      String
"Type2<Type3,#y,Type3>" String
"Type2<#x,#y,#x>"
      (forall a (f :: * -> *). (Mergeable a, Foldable f) => f a -> a
mergeAll [forall a. a -> MergeTree a
mergeLeaf (String
"#x",String
"Type3",Variance
Contravariant),
                 forall a. a -> MergeTree a
mergeLeaf (String
"#x",String
"Type3",Variance
Covariant)]),
    [(String, [String])]
-> [String] -> String -> String -> IO (TrackedErrors ())
checkInferenceFail
      [(String
"#x",[]),(String
"#y",[])] [String
"#x"]
      String
"Type2<Type3,Type0,Type3>" String
"Type2<#x,#y,#x>",

    [(String, [String])]
-> [String]
-> String
-> String
-> MergeTree (String, String, Variance)
-> IO (TrackedErrors ())
checkInferenceSuccess
      [(String
"#x",[]),(String
"#y",[])] [String
"#x"]
      String
"Type2<Type3,#y,Type0>" String
"Type1<#x>"
      (forall a. a -> MergeTree a
mergeLeaf (String
"#x",String
"Type3",Variance
Invariant)),

    [(String, [String])]
-> [String]
-> String
-> String
-> MergeTree (String, String, Variance)
-> IO (TrackedErrors ())
checkInferenceSuccess
      [(String
"#x",[]),(String
"#y",[])] [String
"#x"]
      String
"Instance1<#y>" String
"Instance1<#x>"
      (forall a. a -> MergeTree a
mergeLeaf (String
"#x",String
"#y",Variance
Contravariant)),

    [(String, [String])]
-> [String]
-> String
-> String
-> MergeTree (String, String, Variance)
-> IO (TrackedErrors ())
checkInferenceSuccess
      [(String
"#x",[])] [String
"#x"]
      String
"Instance1<Instance0>" String
"Instance1<[#x&Type0]>"
      (forall a. a -> MergeTree a
mergeLeaf (String
"#x",String
"Instance0",Variance
Contravariant)),
    [(String, [String])]
-> [String] -> String -> String -> IO (TrackedErrors ())
checkInferenceFail
      [(String
"#x",[])] [String
"#x"]
      String
"Instance1<Instance0>" String
"Instance1<[#x|Type0]>",
    [(String, [String])]
-> [String]
-> String
-> String
-> MergeTree (String, String, Variance)
-> IO (TrackedErrors ())
checkInferenceSuccess
      [(String
"#x",[])] [String
"#x"]
      String
"Instance1<Type1<Type0>>" String
"Instance1<[Type0&Type1<#x>]>"
      (forall a. a -> MergeTree a
mergeLeaf (String
"#x",String
"Type0",Variance
Invariant)),
    [(String, [String])]
-> [String]
-> String
-> String
-> MergeTree (String, String, Variance)
-> IO (TrackedErrors ())
checkInferenceSuccess
      [(String
"#x",[])] [String
"#x"]
      String
"Instance1<Type1<Type0>>" String
"Instance1<[#x&Type1<#x>]>"
      (forall a (f :: * -> *). (Mergeable a, Foldable f) => f a -> a
mergeAny [forall a. a -> MergeTree a
mergeLeaf (String
"#x",String
"Type0",Variance
Invariant),
                 forall a. a -> MergeTree a
mergeLeaf (String
"#x",String
"Type1<Type0>",Variance
Contravariant)]),

    [(String, [String])]
-> [String]
-> String
-> String
-> MergeTree (String, String, Variance)
-> IO (TrackedErrors ())
checkInferenceSuccess
      [(String
"#x",[]),(String
"#y",[String
"allows #x"])] [String
"#x"]
      String
"Type0" String
"#y"  -- The filter for #y influences the guess for #x.
      (forall a. a -> MergeTree a
mergeLeaf (String
"#x",String
"Type0",Variance
Covariant))
  ]


type0 :: CategoryName
type0 :: CategoryName
type0 = String -> CategoryName
CategoryName String
"Type0"

type1 :: CategoryName
type1 :: CategoryName
type1 = String -> CategoryName
CategoryName String
"Type1"

type2 :: CategoryName
type2 :: CategoryName
type2 = String -> CategoryName
CategoryName String
"Type2"

type3 :: CategoryName
type3 :: CategoryName
type3 = String -> CategoryName
CategoryName String
"Type3"

type4 :: CategoryName
type4 :: CategoryName
type4 = String -> CategoryName
CategoryName String
"Type4"

type5 :: CategoryName
type5 :: CategoryName
type5 = String -> CategoryName
CategoryName String
"Type5"

instance0 :: CategoryName
instance0 :: CategoryName
instance0 = String -> CategoryName
CategoryName String
"Instance0"

instance1 :: CategoryName
instance1 :: CategoryName
instance1 = String -> CategoryName
CategoryName String
"Instance1"

variances :: Map.Map CategoryName InstanceVariances
variances :: Map CategoryName InstanceVariances
variances = forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList forall a b. (a -> b) -> a -> b
$ [
    (CategoryName
type0,forall a. [a] -> Positional a
Positional []), -- Type0<>
    (CategoryName
type1,forall a. [a] -> Positional a
Positional [Variance
Invariant]), -- Type1<x>
    (CategoryName
type2,forall a. [a] -> Positional a
Positional [Variance
Contravariant,Variance
Invariant,Variance
Covariant]), -- Type2<x|y|z>
    (CategoryName
type3,forall a. [a] -> Positional a
Positional []), -- Type3<>
    (CategoryName
type4,forall a. [a] -> Positional a
Positional [Variance
Invariant]), -- Type4<x>
    (CategoryName
type5,forall a. [a] -> Positional a
Positional [Variance
Invariant]), -- Type5<x>
    (CategoryName
instance0,forall a. [a] -> Positional a
Positional []), -- Instance0<>
    (CategoryName
instance1,forall a. [a] -> Positional a
Positional [Variance
Contravariant]) -- Instance1<x|>
  ]

refines :: Map.Map CategoryName (Map.Map CategoryName (InstanceParams -> InstanceParams))
refines :: Map
  CategoryName (Map CategoryName (InstanceParams -> InstanceParams))
refines = forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList forall a b. (a -> b) -> a -> b
$ [
    (CategoryName
type0,forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList forall a b. (a -> b) -> a -> b
$ []),
    (CategoryName
type1,forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList forall a b. (a -> b) -> a -> b
$ [
        -- Type1<x> -> Type0
        (CategoryName
type0,\(Positional [GeneralInstance
_]) ->
               forall a. [a] -> Positional a
Positional [])
      ]),
    (CategoryName
type2,forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList forall a b. (a -> b) -> a -> b
$ [
        -- Type2<x,y,z> -> Type0 (inherited from Type1)
        (CategoryName
type0,\(Positional [GeneralInstance
_,GeneralInstance
_,GeneralInstance
_]) ->
               forall a. [a] -> Positional a
Positional []),
        -- Type2<x,y,z> -> Type1<x>
        (CategoryName
type1,\(Positional [GeneralInstance
x,GeneralInstance
_,GeneralInstance
_]) ->
               forall a. [a] -> Positional a
Positional [GeneralInstance
x])
      ]),
    (CategoryName
type3,forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList forall a b. (a -> b) -> a -> b
$ [
        -- Type3 -> Type0
        (CategoryName
type0,\(Positional []) ->
               forall a. [a] -> Positional a
Positional [])
      ]),
    (CategoryName
type4,forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList forall a b. (a -> b) -> a -> b
$ []),
    (CategoryName
type5,forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList forall a b. (a -> b) -> a -> b
$ [])
  ]

defines :: Map.Map CategoryName (Map.Map CategoryName (InstanceParams -> InstanceParams))
defines :: Map
  CategoryName (Map CategoryName (InstanceParams -> InstanceParams))
defines = forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList forall a b. (a -> b) -> a -> b
$ [
    (CategoryName
type0,forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList forall a b. (a -> b) -> a -> b
$ [
        -- Type0 defines Instance1<Type0>
        (CategoryName
instance1,\(Positional []) ->
                   forall a. [a] -> Positional a
Positional [forall a. ParseFromSource a => String -> a
forceParse String
"Type0"])
      ]),
    (CategoryName
type1,forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList forall a b. (a -> b) -> a -> b
$ []),
    (CategoryName
type2,forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList forall a b. (a -> b) -> a -> b
$ []),
    (CategoryName
type3,forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList forall a b. (a -> b) -> a -> b
$ [
        -- Type3 defines Instance0
        (CategoryName
instance0,\(Positional []) ->
                   forall a. [a] -> Positional a
Positional [])
      ]),
    (CategoryName
type4,forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList forall a b. (a -> b) -> a -> b
$ []),
    (CategoryName
type5,forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList forall a b. (a -> b) -> a -> b
$ [])
  ]

typeFilters :: Map.Map CategoryName (InstanceParams -> InstanceFilters)
typeFilters :: Map CategoryName (InstanceParams -> InstanceFilters)
typeFilters = forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList forall a b. (a -> b) -> a -> b
$ [
    (CategoryName
type0,\(Positional []) -> forall a. [a] -> Positional a
Positional []),
    (CategoryName
type1,\(Positional [GeneralInstance
_]) ->
           forall a. [a] -> Positional a
Positional [
             -- x requires Type0
             -- x defines Instance0
             [forall a. ParseFromSource a => String -> a
forceParse String
"requires Type0",forall a. ParseFromSource a => String -> a
forceParse String
"defines Instance0"]
           ]),
    (CategoryName
type2,\(Positional [GeneralInstance
_,GeneralInstance
y,GeneralInstance
_]) ->
           forall a. [a] -> Positional a
Positional [
             -- x defines Instance1<Type3>
             [forall a. ParseFromSource a => String -> a
forceParse forall a b. (a -> b) -> a -> b
$ String
"defines Instance1<Type3>"],
             -- y defines Instance1<y>
             [forall a. ParseFromSource a => String -> a
forceParse forall a b. (a -> b) -> a -> b
$ String
"defines Instance1<" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show GeneralInstance
y forall a. [a] -> [a] -> [a]
++ String
">"],
             -- z defines Instance1<Type0>
             [forall a. ParseFromSource a => String -> a
forceParse forall a b. (a -> b) -> a -> b
$ String
"defines Instance1<Type0>"]
           ]),
    (CategoryName
type3,\(Positional []) -> forall a. [a] -> Positional a
Positional []),
    (CategoryName
type4,\(Positional [GeneralInstance
_]) ->
           forall a. [a] -> Positional a
Positional [
             -- x allows Type0
             [forall a. ParseFromSource a => String -> a
forceParse String
"allows Type0"]
           ]),
    (CategoryName
type5,\(Positional [GeneralInstance
_]) -> forall a. [a] -> Positional a
Positional [[]])
  ]

definesFilters :: Map.Map CategoryName (InstanceParams -> InstanceFilters)
definesFilters :: Map CategoryName (InstanceParams -> InstanceFilters)
definesFilters = forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList forall a b. (a -> b) -> a -> b
$ [
    (CategoryName
instance0,\(Positional []) -> forall a. [a] -> Positional a
Positional []),
    (CategoryName
instance1,\(Positional [GeneralInstance
_]) ->
           forall a. [a] -> Positional a
Positional [
             -- x requires Type0
             [forall a. ParseFromSource a => String -> a
forceParse String
"requires Type0"]
           ])
  ]

checkParseSuccess :: String -> GeneralInstance -> IO (TrackedErrors ())
checkParseSuccess :: String -> GeneralInstance -> IO (TrackedErrors ())
checkParseSuccess String
x GeneralInstance
y = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ do
  GeneralInstance
t <- forall a. ParseFromSource a => String -> String -> TrackedErrors a
readSingle String
"(string)" String
x forall (m :: * -> *) a. ErrorContextM m => m a -> String -> m a
<!! (String
"When parsing " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show String
x)
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (GeneralInstance
t forall a. Eq a => a -> a -> Bool
/= GeneralInstance
y) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. ErrorContextM m => String -> m a
compilerErrorM forall a b. (a -> b) -> a -> b
$ String
"Expected " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show String
x forall a. [a] -> [a] -> [a]
++ String
" to parse as " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show GeneralInstance
y

checkParseFail :: String -> IO (TrackedErrors ())
checkParseFail :: String -> IO (TrackedErrors ())
checkParseFail String
x = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ do
  let t :: TrackedErrorsT Identity GeneralInstance
t = forall a. ParseFromSource a => String -> String -> TrackedErrors a
readSingle String
"(string)" String
x :: TrackedErrors GeneralInstance
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall (t :: (* -> *) -> * -> *) a.
(ErrorContextT t, ErrorContextM (t Identity)) =>
t Identity a -> Bool
isCompilerError TrackedErrorsT Identity GeneralInstance
t) forall a b. (a -> b) -> a -> b
$
    forall (m :: * -> *) a. ErrorContextM m => String -> m a
compilerErrorM forall a b. (a -> b) -> a -> b
$ String
"Expected failure to parse " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show String
x forall a. [a] -> [a] -> [a]
++
                    String
" but got " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall a. TrackedErrors a -> a
getCompilerSuccess TrackedErrorsT Identity GeneralInstance
t)

checkSimpleConvertSuccess :: String -> String -> IO (TrackedErrors ())
checkSimpleConvertSuccess :: String -> String -> IO (TrackedErrors ())
checkSimpleConvertSuccess = [(String, [String])] -> String -> String -> IO (TrackedErrors ())
checkConvertSuccess []

checkSimpleConvertFail :: String -> String -> IO (TrackedErrors ())
checkSimpleConvertFail :: String -> String -> IO (TrackedErrors ())
checkSimpleConvertFail = [(String, [String])] -> String -> String -> IO (TrackedErrors ())
checkConvertFail []

checkConvertSuccess :: [(String, [String])] -> String -> String -> IO (TrackedErrors ())
checkConvertSuccess :: [(String, [String])] -> String -> String -> IO (TrackedErrors ())
checkConvertSuccess [(String, [String])]
pa String
x String
y = forall (m :: * -> *) a. Monad m => a -> m a
return TrackedErrors ()
checked where
  prefix :: String
prefix = String
x forall a. [a] -> [a] -> [a]
++ String
" -> " forall a. [a] -> [a] -> [a]
++ String
y forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ [(String, [String])] -> String
showFilters [(String, [String])]
pa
  checked :: TrackedErrors ()
checked = do
    ([ValueType
t1,ValueType
t2],ParamFilters
pa2) <- forall a.
ParseFromSource a =>
[(String, [String])]
-> [String] -> TrackedErrors ([a], ParamFilters)
parseTestWithFilters [(String, [String])]
pa [String
x,String
y]
    forall {m :: * -> *} {a}.
ErrorContextM m =>
TrackedErrorsT Identity a -> m ()
check forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) r.
(CollectErrorsM m, TypeResolver r) =>
r -> ParamFilters -> ValueType -> ValueType -> m ()
checkValueAssignment Resolver
Resolver ParamFilters
pa2 ValueType
t1 ValueType
t2
  check :: TrackedErrorsT Identity a -> m ()
check TrackedErrorsT Identity a
c
    | forall (t :: (* -> *) -> * -> *) a.
(ErrorContextT t, ErrorContextM (t Identity)) =>
t Identity a -> Bool
isCompilerError TrackedErrorsT Identity a
c = forall (m :: * -> *) a. ErrorContextM m => String -> m a
compilerErrorM forall a b. (a -> b) -> a -> b
$ String
prefix forall a. [a] -> [a] -> [a]
++ String
":\n" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall a. TrackedErrors a -> CompilerMessage
getCompilerError TrackedErrorsT Identity a
c)
    | Bool
otherwise = forall (m :: * -> *) a. Monad m => a -> m a
return ()

checkInferenceSuccess :: [(String, [String])] -> [String] -> String ->
  String -> MergeTree (String,String,Variance) -> IO (TrackedErrors ())
checkInferenceSuccess :: [(String, [String])]
-> [String]
-> String
-> String
-> MergeTree (String, String, Variance)
-> IO (TrackedErrors ())
checkInferenceSuccess [(String, [String])]
pa [String]
is String
x String
y MergeTree (String, String, Variance)
gs = (MergeTree InferredTypeGuess
 -> TrackedErrors (MergeTree InferredTypeGuess) -> TrackedErrors ())
-> [(String, [String])]
-> [String]
-> String
-> String
-> MergeTree (String, String, Variance)
-> IO (TrackedErrors ())
checkInferenceCommon forall {a}.
(Eq a, Show a) =>
a -> TrackedErrorsT Identity a -> TrackedErrors ()
check [(String, [String])]
pa [String]
is String
x String
y MergeTree (String, String, Variance)
gs where
  prefix :: String
prefix = String
x forall a. [a] -> [a] -> [a]
++ String
" -> " forall a. [a] -> [a] -> [a]
++ String
y forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ [(String, [String])] -> String
showFilters [(String, [String])]
pa
  check :: a -> TrackedErrorsT Identity a -> TrackedErrors ()
check a
gs2 TrackedErrorsT Identity a
c
    | forall (t :: (* -> *) -> * -> *) a.
(ErrorContextT t, ErrorContextM (t Identity)) =>
t Identity a -> Bool
isCompilerError TrackedErrorsT Identity a
c = forall (m :: * -> *) a. ErrorContextM m => String -> m a
compilerErrorM forall a b. (a -> b) -> a -> b
$ String
prefix forall a. [a] -> [a] -> [a]
++ String
":\n" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall a. TrackedErrors a -> CompilerMessage
getCompilerError TrackedErrorsT Identity a
c)
    | Bool
otherwise        = forall a. TrackedErrors a -> a
getCompilerSuccess TrackedErrorsT Identity a
c forall a. (Eq a, Show a) => a -> a -> TrackedErrors ()
`checkEquals` a
gs2

checkInferenceFail :: [(String, [String])] -> [String] -> String ->
  String -> IO (TrackedErrors ())
checkInferenceFail :: [(String, [String])]
-> [String] -> String -> String -> IO (TrackedErrors ())
checkInferenceFail [(String, [String])]
pa [String]
is String
x String
y = (MergeTree InferredTypeGuess
 -> TrackedErrors (MergeTree InferredTypeGuess) -> TrackedErrors ())
-> [(String, [String])]
-> [String]
-> String
-> String
-> MergeTree (String, String, Variance)
-> IO (TrackedErrors ())
checkInferenceCommon forall {t :: (* -> *) -> * -> *} {m :: * -> *} {p} {a}.
(ErrorContextT t, ErrorContextM m, ErrorContextM (t Identity)) =>
p -> t Identity a -> m ()
check [(String, [String])]
pa [String]
is String
x String
y (forall a (f :: * -> *). (Mergeable a, Foldable f) => f a -> a
mergeAll []) where
  prefix :: String
prefix = String
x forall a. [a] -> [a] -> [a]
++ String
" -> " forall a. [a] -> [a] -> [a]
++ String
y forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ [(String, [String])] -> String
showFilters [(String, [String])]
pa
  check :: p -> t Identity a -> m ()
check p
_ t Identity a
c
    | forall (t :: (* -> *) -> * -> *) a.
(ErrorContextT t, ErrorContextM (t Identity)) =>
t Identity a -> Bool
isCompilerError t Identity a
c = forall (m :: * -> *) a. Monad m => a -> m a
return ()
    | Bool
otherwise = forall (m :: * -> *) a. ErrorContextM m => String -> m a
compilerErrorM forall a b. (a -> b) -> a -> b
$ String
prefix forall a. [a] -> [a] -> [a]
++ String
": Expected failure\n"

checkInferenceCommon ::
  (MergeTree InferredTypeGuess -> TrackedErrors (MergeTree InferredTypeGuess) -> TrackedErrors ()) ->
  [(String, [String])] -> [String] -> String -> String ->
  MergeTree (String,String,Variance) -> IO (TrackedErrors ())
checkInferenceCommon :: (MergeTree InferredTypeGuess
 -> TrackedErrors (MergeTree InferredTypeGuess) -> TrackedErrors ())
-> [(String, [String])]
-> [String]
-> String
-> String
-> MergeTree (String, String, Variance)
-> IO (TrackedErrors ())
checkInferenceCommon MergeTree InferredTypeGuess
-> TrackedErrors (MergeTree InferredTypeGuess) -> TrackedErrors ()
check [(String, [String])]
pa [String]
is String
x String
y MergeTree (String, String, Variance)
gs = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ TrackedErrors ()
checked forall (m :: * -> *) a. ErrorContextM m => m a -> String -> m a
<!! String
context where
  context :: String
context = String
"With params = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show [(String, [String])]
pa forall a. [a] -> [a] -> [a]
++ String
", pair = (" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show String
x forall a. [a] -> [a] -> [a]
++ String
"," forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show String
y forall a. [a] -> [a] -> [a]
++ String
")"
  checked :: TrackedErrors ()
checked = do
    ([GeneralInstance
t1,GeneralInstance
t2],ParamFilters
pa2) <- forall a.
ParseFromSource a =>
[(String, [String])]
-> [String] -> TrackedErrors ([a], ParamFilters)
parseTestWithFilters [(String, [String])]
pa [String
x,String
y]
    [(ParamName, GeneralInstance)]
ia2 <- forall (m :: * -> *) a b.
CollectErrorsM m =>
(a -> m b) -> [a] -> m [b]
mapCompilerM String -> TrackedErrorsT Identity (ParamName, GeneralInstance)
readInferred [String]
is
    MergeTree InferredTypeGuess
gs' <- forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (String, String, Variance)
-> TrackedErrorsT Identity InferredTypeGuess
parseGuess MergeTree (String, String, Variance)
gs
    let iaMap :: Map ParamName GeneralInstance
iaMap = forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(ParamName, GeneralInstance)]
ia2
    -- TODO: Merge duplication with Test.TypeCategory.
    ParamFilters
pa3 <- forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a b.
CollectErrorsM m =>
(a -> m b) -> [a] -> m [b]
mapCompilerM (forall {m :: * -> *} {a}.
CollectErrorsM m =>
Map ParamName GeneralInstance
-> (a, [TypeFilter]) -> m (a, [TypeFilter])
filterSub Map ParamName GeneralInstance
iaMap) forall a b. (a -> b) -> a -> b
$ forall k a. Map k a -> [(k, a)]
Map.toList ParamFilters
pa2
    GeneralInstance
t2' <- forall (m :: * -> *).
CollectErrorsM m =>
(ParamName -> m GeneralInstance)
-> GeneralInstance -> m GeneralInstance
uncheckedSubInstance (forall {m :: * -> *}.
Monad m =>
Map ParamName GeneralInstance -> ParamName -> m GeneralInstance
weakLookup Map ParamName GeneralInstance
iaMap) GeneralInstance
t2
    MergeTree InferredTypeGuess
-> TrackedErrors (MergeTree InferredTypeGuess) -> TrackedErrors ()
check MergeTree InferredTypeGuess
gs' forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) r.
(CollectErrorsM m, TypeResolver r) =>
r
-> ParamFilters
-> Variance
-> GeneralInstance
-> GeneralInstance
-> m (MergeTree InferredTypeGuess)
checkGeneralMatch Resolver
Resolver ParamFilters
pa3 Variance
Covariant GeneralInstance
t1 GeneralInstance
t2'
  readInferred :: String -> TrackedErrorsT Identity (ParamName, GeneralInstance)
readInferred String
p = do
    ParamName
p' <- forall a. ParseFromSource a => String -> String -> TrackedErrors a
readSingle String
"(string)" String
p
    forall (m :: * -> *) a. Monad m => a -> m a
return (ParamName
p',forall a. (Eq a, Ord a) => a -> GeneralType a
singleType forall a b. (a -> b) -> a -> b
$ ParamName -> TypeInstanceOrParam
JustInferredType ParamName
p')
  parseGuess :: (String, String, Variance)
-> TrackedErrorsT Identity InferredTypeGuess
parseGuess (String
p,String
t,Variance
v) = do
    ParamName
p' <- forall a. ParseFromSource a => String -> String -> TrackedErrors a
readSingle String
"(string)" String
p
    GeneralInstance
t' <- forall a. ParseFromSource a => String -> String -> TrackedErrors a
readSingle String
"(string)" String
t
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ ParamName -> GeneralInstance -> Variance -> InferredTypeGuess
InferredTypeGuess ParamName
p' GeneralInstance
t' Variance
v
  weakLookup :: Map ParamName GeneralInstance -> ParamName -> m GeneralInstance
weakLookup Map ParamName GeneralInstance
tm ParamName
n =
    case ParamName
n forall k a. Ord k => k -> Map k a -> Maybe a
`Map.lookup` Map ParamName GeneralInstance
tm of
         Just GeneralInstance
t  -> forall (m :: * -> *) a. Monad m => a -> m a
return GeneralInstance
t
         Maybe GeneralInstance
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. (Eq a, Ord a) => a -> GeneralType a
singleType forall a b. (a -> b) -> a -> b
$ Bool -> ParamName -> TypeInstanceOrParam
JustParamName Bool
True ParamName
n
  filterSub :: Map ParamName GeneralInstance
-> (a, [TypeFilter]) -> m (a, [TypeFilter])
filterSub Map ParamName GeneralInstance
im (a
k,[TypeFilter]
fs) = do
    [TypeFilter]
fs' <- forall (m :: * -> *) a b.
CollectErrorsM m =>
(a -> m b) -> [a] -> m [b]
mapCompilerM (forall (m :: * -> *).
CollectErrorsM m =>
(ParamName -> m GeneralInstance) -> TypeFilter -> m TypeFilter
uncheckedSubFilter (forall {m :: * -> *}.
Monad m =>
Map ParamName GeneralInstance -> ParamName -> m GeneralInstance
weakLookup Map ParamName GeneralInstance
im)) [TypeFilter]
fs
    forall (m :: * -> *) a. Monad m => a -> m a
return (a
k,[TypeFilter]
fs')

checkConvertFail :: [(String, [String])] -> String -> String -> IO (TrackedErrors ())
checkConvertFail :: [(String, [String])] -> String -> String -> IO (TrackedErrors ())
checkConvertFail [(String, [String])]
pa String
x String
y = forall (m :: * -> *) a. Monad m => a -> m a
return TrackedErrors ()
checked where
  prefix :: String
prefix = String
x forall a. [a] -> [a] -> [a]
++ String
" /> " forall a. [a] -> [a] -> [a]
++ String
y forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ [(String, [String])] -> String
showFilters [(String, [String])]
pa
  checked :: TrackedErrors ()
checked = do
    ([ValueType
t1,ValueType
t2],ParamFilters
pa2) <- forall a.
ParseFromSource a =>
[(String, [String])]
-> [String] -> TrackedErrors ([a], ParamFilters)
parseTestWithFilters [(String, [String])]
pa [String
x,String
y]
    forall a. TrackedErrors a -> TrackedErrors ()
check forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) r.
(CollectErrorsM m, TypeResolver r) =>
r -> ParamFilters -> ValueType -> ValueType -> m ()
checkValueAssignment Resolver
Resolver ParamFilters
pa2 ValueType
t1 ValueType
t2
  check :: TrackedErrors a -> TrackedErrors ()
  check :: forall a. TrackedErrors a -> TrackedErrors ()
check TrackedErrors a
c
    | forall (t :: (* -> *) -> * -> *) a.
(ErrorContextT t, ErrorContextM (t Identity)) =>
t Identity a -> Bool
isCompilerError TrackedErrors a
c = forall (m :: * -> *) a. Monad m => a -> m a
return ()
    | Bool
otherwise = forall (m :: * -> *) a. ErrorContextM m => String -> m a
compilerErrorM forall a b. (a -> b) -> a -> b
$ String
prefix forall a. [a] -> [a] -> [a]
++ String
": Expected failure\n"

data Resolver = Resolver

instance TypeResolver Resolver where
  trRefines :: forall (m :: * -> *).
CollectErrorsM m =>
Resolver -> TypeInstance -> CategoryName -> m InstanceParams
trRefines Resolver
_ = forall (m :: * -> *).
CollectErrorsM m =>
Map
  CategoryName (Map CategoryName (InstanceParams -> InstanceParams))
-> TypeInstance -> CategoryName -> m InstanceParams
getParams Map
  CategoryName (Map CategoryName (InstanceParams -> InstanceParams))
refines
  trDefines :: forall (m :: * -> *).
CollectErrorsM m =>
Resolver -> TypeInstance -> CategoryName -> m InstanceParams
trDefines Resolver
_ = forall (m :: * -> *).
CollectErrorsM m =>
Map
  CategoryName (Map CategoryName (InstanceParams -> InstanceParams))
-> TypeInstance -> CategoryName -> m InstanceParams
getParams Map
  CategoryName (Map CategoryName (InstanceParams -> InstanceParams))
defines
  trVariance :: forall (m :: * -> *).
CollectErrorsM m =>
Resolver -> CategoryName -> m InstanceVariances
trVariance Resolver
_ = forall n (m :: * -> *) a.
(Ord n, Show n, CollectErrorsM m) =>
Map n a -> n -> m a
mapLookup Map CategoryName InstanceVariances
variances
  trTypeFilters :: forall (m :: * -> *).
CollectErrorsM m =>
Resolver -> TypeInstance -> m InstanceFilters
trTypeFilters Resolver
_ = forall (m :: * -> *).
CollectErrorsM m =>
TypeInstance -> m InstanceFilters
getTypeFilters
  trDefinesFilters :: forall (m :: * -> *).
CollectErrorsM m =>
Resolver -> DefinesInstance -> m InstanceFilters
trDefinesFilters Resolver
_ = forall (m :: * -> *).
CollectErrorsM m =>
DefinesInstance -> m InstanceFilters
getDefinesFilters
  -- Type5 is concrete, somewhat arbitrarily.
  trConcrete :: forall (m :: * -> *).
CollectErrorsM m =>
Resolver -> CategoryName -> m Bool
trConcrete Resolver
_ = \CategoryName
t -> forall (m :: * -> *) a. Monad m => a -> m a
return (CategoryName
t forall a. Eq a => a -> a -> Bool
== CategoryName
type5)
  trImmutable :: forall (m :: * -> *).
CollectErrorsM m =>
Resolver -> CategoryName -> m Bool
trImmutable Resolver
_ CategoryName
_ = forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False

getParams :: CollectErrorsM m =>
  Map.Map CategoryName (Map.Map CategoryName (InstanceParams -> InstanceParams))
  -> TypeInstance -> CategoryName -> m InstanceParams
getParams :: forall (m :: * -> *).
CollectErrorsM m =>
Map
  CategoryName (Map CategoryName (InstanceParams -> InstanceParams))
-> TypeInstance -> CategoryName -> m InstanceParams
getParams Map
  CategoryName (Map CategoryName (InstanceParams -> InstanceParams))
ma (TypeInstance CategoryName
n1 InstanceParams
ps1) CategoryName
n2 = do
  Map CategoryName (InstanceParams -> InstanceParams)
ra <- forall n (m :: * -> *) a.
(Ord n, Show n, CollectErrorsM m) =>
Map n a -> n -> m a
mapLookup Map
  CategoryName (Map CategoryName (InstanceParams -> InstanceParams))
ma CategoryName
n1 forall (m :: * -> *) a. ErrorContextM m => m a -> String -> m a
<?? String
"In lookup of category " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show CategoryName
n1
  InstanceParams -> InstanceParams
f <- forall n (m :: * -> *) a.
(Ord n, Show n, CollectErrorsM m) =>
Map n a -> n -> m a
mapLookup Map CategoryName (InstanceParams -> InstanceParams)
ra CategoryName
n2 forall (m :: * -> *) a. ErrorContextM m => m a -> String -> m a
<?? String
"In lookup of parent " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show CategoryName
n2 forall a. [a] -> [a] -> [a]
++ String
" of " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show CategoryName
n1
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ InstanceParams -> InstanceParams
f InstanceParams
ps1

getTypeFilters :: CollectErrorsM m => TypeInstance -> m InstanceFilters
getTypeFilters :: forall (m :: * -> *).
CollectErrorsM m =>
TypeInstance -> m InstanceFilters
getTypeFilters (TypeInstance CategoryName
n InstanceParams
ps) = String
"In type filters lookup" forall (m :: * -> *) a. ErrorContextM m => String -> m a -> m a
??> do
  InstanceParams -> InstanceFilters
f <- forall n (m :: * -> *) a.
(Ord n, Show n, CollectErrorsM m) =>
Map n a -> n -> m a
mapLookup Map CategoryName (InstanceParams -> InstanceFilters)
typeFilters CategoryName
n
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ InstanceParams -> InstanceFilters
f InstanceParams
ps

getDefinesFilters :: CollectErrorsM m => DefinesInstance -> m InstanceFilters
getDefinesFilters :: forall (m :: * -> *).
CollectErrorsM m =>
DefinesInstance -> m InstanceFilters
getDefinesFilters (DefinesInstance CategoryName
n InstanceParams
ps) = String
"In defines filters lookup" forall (m :: * -> *) a. ErrorContextM m => String -> m a -> m a
??> do
  InstanceParams -> InstanceFilters
f <- forall n (m :: * -> *) a.
(Ord n, Show n, CollectErrorsM m) =>
Map n a -> n -> m a
mapLookup Map CategoryName (InstanceParams -> InstanceFilters)
definesFilters CategoryName
n
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ InstanceParams -> InstanceFilters
f InstanceParams
ps

mapLookup :: (Ord n, Show n, CollectErrorsM m) => Map.Map n a -> n -> m a
mapLookup :: forall n (m :: * -> *) a.
(Ord n, Show n, CollectErrorsM m) =>
Map n a -> n -> m a
mapLookup Map n a
ma n
n = forall {m :: * -> *} {a}. ErrorContextM m => Maybe a -> m a
resolve forall a b. (a -> b) -> a -> b
$ n
n forall k a. Ord k => k -> Map k a -> Maybe a
`Map.lookup` Map n a
ma where
  resolve :: Maybe a -> m a
resolve (Just a
x) = forall (m :: * -> *) a. Monad m => a -> m a
return a
x
  resolve Maybe a
_        = forall (m :: * -> *) a. ErrorContextM m => String -> m a
compilerErrorM forall a b. (a -> b) -> a -> b
$ String
"Map key " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show n
n forall a. [a] -> [a] -> [a]
++ String
" not found"