{-# LANGUAGE CPP
           , ScopedTypeVariables
           , GADTs
           , DataKinds
           , KindSignatures
           , GeneralizedNewtypeDeriving
           , TypeOperators
           , FlexibleContexts
           , FlexibleInstances
           , OverloadedStrings
           , PatternGuards
           , Rank2Types
           #-}

{-# OPTIONS_GHC -Wall -fwarn-tabs #-}
----------------------------------------------------------------
-- |
-- Module      :  Language.Hakaru.Syntax.TypeCheck
-- Copyright   :  Copyright (c) 2017 the Hakaru team
-- License     :  BSD3
-- Stability   :  experimental
-- Portability :  GHC-only
--
-- Bidirectional type checking for our AST.
----------------------------------------------------------------
module Language.Hakaru.Syntax.TypeCheck.TypeCheckMonad where

import           Prelude hiding (id, (.))
import           Control.Category
import           Data.Proxy            (KProxy(..))
import           Data.Text             (Text())
import qualified Data.Vector           as V
#if __GLASGOW_HASKELL__ < 710
import           Control.Applicative   (Applicative(..), (<$>))
import           Data.Monoid           (Monoid(..))
#endif
#if __GLASGOW_HASKELL__ > 805
import           Control.Monad.Fail
#endif
import qualified Language.Hakaru.Parser.AST as U

import Language.Hakaru.Syntax.IClasses
import Language.Hakaru.Types.DataKind (Hakaru(..), HData', HBool)
import Language.Hakaru.Types.Sing
import Language.Hakaru.Types.Coercion
import Language.Hakaru.Types.HClasses
    ( HEq, hEq_Sing, HOrd, hOrd_Sing, HSemiring, hSemiring_Sing
    , hRing_Sing, sing_HRing, hFractional_Sing)
import Language.Hakaru.Syntax.ABT
import Language.Hakaru.Syntax.Datum
import Language.Hakaru.Syntax.Reducer
import Language.Hakaru.Syntax.AST
import Language.Hakaru.Pretty.Concrete (prettyTypeT)

-- | * Definition of the typechecking monad and related
-- types\/functions\/instances.

type Input = Maybe (V.Vector Text)

type Ctx = VarSet ('KProxy :: KProxy Hakaru)

data TypeCheckMode = StrictMode | LaxMode | UnsafeMode
    deriving (ReadPrec [TypeCheckMode]
ReadPrec TypeCheckMode
Int -> ReadS TypeCheckMode
ReadS [TypeCheckMode]
(Int -> ReadS TypeCheckMode)
-> ReadS [TypeCheckMode]
-> ReadPrec TypeCheckMode
-> ReadPrec [TypeCheckMode]
-> Read TypeCheckMode
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [TypeCheckMode]
$creadListPrec :: ReadPrec [TypeCheckMode]
readPrec :: ReadPrec TypeCheckMode
$creadPrec :: ReadPrec TypeCheckMode
readList :: ReadS [TypeCheckMode]
$creadList :: ReadS [TypeCheckMode]
readsPrec :: Int -> ReadS TypeCheckMode
$creadsPrec :: Int -> ReadS TypeCheckMode
Read, Int -> TypeCheckMode -> ShowS
[TypeCheckMode] -> ShowS
TypeCheckMode -> String
(Int -> TypeCheckMode -> ShowS)
-> (TypeCheckMode -> String)
-> ([TypeCheckMode] -> ShowS)
-> Show TypeCheckMode
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [TypeCheckMode] -> ShowS
$cshowList :: [TypeCheckMode] -> ShowS
show :: TypeCheckMode -> String
$cshow :: TypeCheckMode -> String
showsPrec :: Int -> TypeCheckMode -> ShowS
$cshowsPrec :: Int -> TypeCheckMode -> ShowS
Show)

type TypeCheckError = Text

newtype TypeCheckMonad a =
    TCM { TypeCheckMonad a
-> Ctx -> Input -> TypeCheckMode -> Either TypeCheckError a
unTCM :: Ctx
                -> Input
                -> TypeCheckMode
                -> Either TypeCheckError a }

runTCM :: TypeCheckMonad a -> Input -> TypeCheckMode -> Either TypeCheckError a
runTCM :: TypeCheckMonad a
-> Input -> TypeCheckMode -> Either TypeCheckError a
runTCM TypeCheckMonad a
m = TypeCheckMonad a
-> Ctx -> Input -> TypeCheckMode -> Either TypeCheckError a
forall a.
TypeCheckMonad a
-> Ctx -> Input -> TypeCheckMode -> Either TypeCheckError a
unTCM TypeCheckMonad a
m Ctx
forall k (kproxy :: KProxy k). VarSet kproxy
emptyVarSet

instance Functor TypeCheckMonad where
    fmap :: (a -> b) -> TypeCheckMonad a -> TypeCheckMonad b
fmap a -> b
f TypeCheckMonad a
m = (Ctx -> Input -> TypeCheckMode -> Either TypeCheckError b)
-> TypeCheckMonad b
forall a.
(Ctx -> Input -> TypeCheckMode -> Either TypeCheckError a)
-> TypeCheckMonad a
TCM ((Ctx -> Input -> TypeCheckMode -> Either TypeCheckError b)
 -> TypeCheckMonad b)
-> (Ctx -> Input -> TypeCheckMode -> Either TypeCheckError b)
-> TypeCheckMonad b
forall a b. (a -> b) -> a -> b
$ \Ctx
ctx Input
input TypeCheckMode
mode -> (a -> b) -> Either TypeCheckError a -> Either TypeCheckError b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f (TypeCheckMonad a
-> Ctx -> Input -> TypeCheckMode -> Either TypeCheckError a
forall a.
TypeCheckMonad a
-> Ctx -> Input -> TypeCheckMode -> Either TypeCheckError a
unTCM TypeCheckMonad a
m Ctx
ctx Input
input TypeCheckMode
mode)

instance Applicative TypeCheckMonad where
    pure :: a -> TypeCheckMonad a
pure a
x    = (Ctx -> Input -> TypeCheckMode -> Either TypeCheckError a)
-> TypeCheckMonad a
forall a.
(Ctx -> Input -> TypeCheckMode -> Either TypeCheckError a)
-> TypeCheckMonad a
TCM ((Ctx -> Input -> TypeCheckMode -> Either TypeCheckError a)
 -> TypeCheckMonad a)
-> (Ctx -> Input -> TypeCheckMode -> Either TypeCheckError a)
-> TypeCheckMonad a
forall a b. (a -> b) -> a -> b
$ \Ctx
_ Input
_ TypeCheckMode
_ -> a -> Either TypeCheckError a
forall a b. b -> Either a b
Right a
x
    TypeCheckMonad (a -> b)
mf <*> :: TypeCheckMonad (a -> b) -> TypeCheckMonad a -> TypeCheckMonad b
<*> TypeCheckMonad a
mx = TypeCheckMonad (a -> b)
mf TypeCheckMonad (a -> b)
-> ((a -> b) -> TypeCheckMonad b) -> TypeCheckMonad b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a -> b
f -> (a -> b) -> TypeCheckMonad a -> TypeCheckMonad b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f TypeCheckMonad a
mx

-- TODO: ensure this instance has the appropriate strictness
instance Monad TypeCheckMonad where
    return :: a -> TypeCheckMonad a
return   = a -> TypeCheckMonad a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
    TypeCheckMonad a
mx >>= :: TypeCheckMonad a -> (a -> TypeCheckMonad b) -> TypeCheckMonad b
>>= a -> TypeCheckMonad b
k =
        (Ctx -> Input -> TypeCheckMode -> Either TypeCheckError b)
-> TypeCheckMonad b
forall a.
(Ctx -> Input -> TypeCheckMode -> Either TypeCheckError a)
-> TypeCheckMonad a
TCM ((Ctx -> Input -> TypeCheckMode -> Either TypeCheckError b)
 -> TypeCheckMonad b)
-> (Ctx -> Input -> TypeCheckMode -> Either TypeCheckError b)
-> TypeCheckMonad b
forall a b. (a -> b) -> a -> b
$ \Ctx
ctx Input
input TypeCheckMode
mode ->
        TypeCheckMonad a
-> Ctx -> Input -> TypeCheckMode -> Either TypeCheckError a
forall a.
TypeCheckMonad a
-> Ctx -> Input -> TypeCheckMode -> Either TypeCheckError a
unTCM TypeCheckMonad a
mx Ctx
ctx Input
input TypeCheckMode
mode Either TypeCheckError a
-> (a -> Either TypeCheckError b) -> Either TypeCheckError b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a
x ->
        TypeCheckMonad b
-> Ctx -> Input -> TypeCheckMode -> Either TypeCheckError b
forall a.
TypeCheckMonad a
-> Ctx -> Input -> TypeCheckMode -> Either TypeCheckError a
unTCM (a -> TypeCheckMonad b
k a
x) Ctx
ctx Input
input TypeCheckMode
mode

#if __GLASGOW_HASKELL__ > 805
instance MonadFail TypeCheckMonad where
    fail :: String -> TypeCheckMonad a
fail = String -> TypeCheckMonad a
forall a. HasCallStack => String -> a
error
#endif

{-
-- We could provide this instance, but there's no decent error
-- message to give for the 'empty' case that works in all circumstances.
-- Because we only would need this to define 'inferOneCheckOthers',
-- we inline the definition there instead.
instance Alternative TypeCheckMonad where
    empty   = failwith "Alternative.empty"
    x <|> y = TCM $ \ctx mode ->
        case unTCM x ctx mode of
        Left  _ -> unTCM y ctx mode
        Right e -> Right e
-}

-- | Return the mode in which we're checking\/inferring types.
getInput :: TypeCheckMonad Input
getInput :: TypeCheckMonad Input
getInput = (Ctx -> Input -> TypeCheckMode -> Either TypeCheckError Input)
-> TypeCheckMonad Input
forall a.
(Ctx -> Input -> TypeCheckMode -> Either TypeCheckError a)
-> TypeCheckMonad a
TCM ((Ctx -> Input -> TypeCheckMode -> Either TypeCheckError Input)
 -> TypeCheckMonad Input)
-> (Ctx -> Input -> TypeCheckMode -> Either TypeCheckError Input)
-> TypeCheckMonad Input
forall a b. (a -> b) -> a -> b
$ \Ctx
_ Input
input TypeCheckMode
_ -> Input -> Either TypeCheckError Input
forall a b. b -> Either a b
Right Input
input

-- | Return the mode in which we're checking\/inferring types.
getMode :: TypeCheckMonad TypeCheckMode
getMode :: TypeCheckMonad TypeCheckMode
getMode = (Ctx
 -> Input -> TypeCheckMode -> Either TypeCheckError TypeCheckMode)
-> TypeCheckMonad TypeCheckMode
forall a.
(Ctx -> Input -> TypeCheckMode -> Either TypeCheckError a)
-> TypeCheckMonad a
TCM ((Ctx
  -> Input -> TypeCheckMode -> Either TypeCheckError TypeCheckMode)
 -> TypeCheckMonad TypeCheckMode)
-> (Ctx
    -> Input -> TypeCheckMode -> Either TypeCheckError TypeCheckMode)
-> TypeCheckMonad TypeCheckMode
forall a b. (a -> b) -> a -> b
$ \Ctx
_ Input
_ TypeCheckMode
mode -> TypeCheckMode -> Either TypeCheckError TypeCheckMode
forall a b. b -> Either a b
Right TypeCheckMode
mode

-- | Extend the typing context, but only locally.
pushCtx
    :: Variable (a :: Hakaru)
    -> TypeCheckMonad b
    -> TypeCheckMonad b
pushCtx :: Variable a -> TypeCheckMonad b -> TypeCheckMonad b
pushCtx Variable a
x (TCM Ctx -> Input -> TypeCheckMode -> Either TypeCheckError b
m) = (Ctx -> Input -> TypeCheckMode -> Either TypeCheckError b)
-> TypeCheckMonad b
forall a.
(Ctx -> Input -> TypeCheckMode -> Either TypeCheckError a)
-> TypeCheckMonad a
TCM (Ctx -> Input -> TypeCheckMode -> Either TypeCheckError b
m (Ctx -> Input -> TypeCheckMode -> Either TypeCheckError b)
-> (Ctx -> Ctx)
-> Ctx
-> Input
-> TypeCheckMode
-> Either TypeCheckError b
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Variable a -> Ctx -> Ctx
forall k (a :: k).
Variable a -> VarSet (KindOf a) -> VarSet (KindOf a)
insertVarSet Variable a
x)

getCtx :: TypeCheckMonad Ctx
getCtx :: TypeCheckMonad Ctx
getCtx = (Ctx -> Input -> TypeCheckMode -> Either TypeCheckError Ctx)
-> TypeCheckMonad Ctx
forall a.
(Ctx -> Input -> TypeCheckMode -> Either TypeCheckError a)
-> TypeCheckMonad a
TCM ((Ctx -> Input -> TypeCheckMode -> Either TypeCheckError Ctx)
 -> TypeCheckMonad Ctx)
-> (Ctx -> Input -> TypeCheckMode -> Either TypeCheckError Ctx)
-> TypeCheckMonad Ctx
forall a b. (a -> b) -> a -> b
$ \Ctx
ctx Input
_ TypeCheckMode
_ -> Ctx -> Either TypeCheckError Ctx
forall a b. b -> Either a b
Right Ctx
ctx

failwith :: TypeCheckError -> TypeCheckMonad r
failwith :: TypeCheckError -> TypeCheckMonad r
failwith TypeCheckError
e = (Ctx -> Input -> TypeCheckMode -> Either TypeCheckError r)
-> TypeCheckMonad r
forall a.
(Ctx -> Input -> TypeCheckMode -> Either TypeCheckError a)
-> TypeCheckMonad a
TCM ((Ctx -> Input -> TypeCheckMode -> Either TypeCheckError r)
 -> TypeCheckMonad r)
-> (Ctx -> Input -> TypeCheckMode -> Either TypeCheckError r)
-> TypeCheckMonad r
forall a b. (a -> b) -> a -> b
$ \Ctx
_ Input
_ TypeCheckMode
_ -> TypeCheckError -> Either TypeCheckError r
forall a b. a -> Either a b
Left TypeCheckError
e

failwith_ :: TypeCheckError -> TypeCheckMonad r
failwith_ :: TypeCheckError -> TypeCheckMonad r
failwith_ = TypeCheckError -> TypeCheckMonad r
forall r. TypeCheckError -> TypeCheckMonad r
failwith

-- TODO: some day we may want a variant of this function which
-- returns the error message in the event that the computation fails
-- (e.g., to provide all of them if 'inferOneCheckOthers' ultimately
-- fails.
--
-- | a la @optional :: Alternative f => f a -> f (Maybe a)@ but
-- without needing the 'empty' of the 'Alternative' class.
try :: TypeCheckMonad a -> TypeCheckMonad (Maybe a)
try :: TypeCheckMonad a -> TypeCheckMonad (Maybe a)
try TypeCheckMonad a
m = (Ctx -> Input -> TypeCheckMode -> Either TypeCheckError (Maybe a))
-> TypeCheckMonad (Maybe a)
forall a.
(Ctx -> Input -> TypeCheckMode -> Either TypeCheckError a)
-> TypeCheckMonad a
TCM ((Ctx -> Input -> TypeCheckMode -> Either TypeCheckError (Maybe a))
 -> TypeCheckMonad (Maybe a))
-> (Ctx
    -> Input -> TypeCheckMode -> Either TypeCheckError (Maybe a))
-> TypeCheckMonad (Maybe a)
forall a b. (a -> b) -> a -> b
$ \Ctx
ctx Input
input TypeCheckMode
mode -> Maybe a -> Either TypeCheckError (Maybe a)
forall a b. b -> Either a b
Right (Maybe a -> Either TypeCheckError (Maybe a))
-> Maybe a -> Either TypeCheckError (Maybe a)
forall a b. (a -> b) -> a -> b
$
    case TypeCheckMonad a
-> Ctx -> Input -> TypeCheckMode -> Either TypeCheckError a
forall a.
TypeCheckMonad a
-> Ctx -> Input -> TypeCheckMode -> Either TypeCheckError a
unTCM TypeCheckMonad a
m Ctx
ctx Input
input TypeCheckMode
mode of
    Left  TypeCheckError
_ -> Maybe a
forall a. Maybe a
Nothing -- Don't worry; no side effects to unwind
    Right a
e -> a -> Maybe a
forall a. a -> Maybe a
Just a
e

-- | Tries to typecheck in a given mode
tryWith :: TypeCheckMode -> TypeCheckMonad a -> TypeCheckMonad (Maybe a)
tryWith :: TypeCheckMode -> TypeCheckMonad a -> TypeCheckMonad (Maybe a)
tryWith TypeCheckMode
mode TypeCheckMonad a
m = (Ctx -> Input -> TypeCheckMode -> Either TypeCheckError (Maybe a))
-> TypeCheckMonad (Maybe a)
forall a.
(Ctx -> Input -> TypeCheckMode -> Either TypeCheckError a)
-> TypeCheckMonad a
TCM ((Ctx -> Input -> TypeCheckMode -> Either TypeCheckError (Maybe a))
 -> TypeCheckMonad (Maybe a))
-> (Ctx
    -> Input -> TypeCheckMode -> Either TypeCheckError (Maybe a))
-> TypeCheckMonad (Maybe a)
forall a b. (a -> b) -> a -> b
$ \Ctx
ctx Input
input TypeCheckMode
_ -> Maybe a -> Either TypeCheckError (Maybe a)
forall a b. b -> Either a b
Right (Maybe a -> Either TypeCheckError (Maybe a))
-> Maybe a -> Either TypeCheckError (Maybe a)
forall a b. (a -> b) -> a -> b
$
    case TypeCheckMonad a
-> Ctx -> Input -> TypeCheckMode -> Either TypeCheckError a
forall a.
TypeCheckMonad a
-> Ctx -> Input -> TypeCheckMode -> Either TypeCheckError a
unTCM TypeCheckMonad a
m Ctx
ctx Input
input TypeCheckMode
mode of
    Left  TypeCheckError
_ -> Maybe a
forall a. Maybe a
Nothing
    Right a
e -> a -> Maybe a
forall a. a -> Maybe a
Just a
e

-- | * Helpers for constructing error messages

makeErrMsg
    :: Text
    -> Maybe U.SourceSpan
    -> Text
    -> TypeCheckMonad TypeCheckError
makeErrMsg :: TypeCheckError
-> Maybe SourceSpan
-> TypeCheckError
-> TypeCheckMonad TypeCheckError
makeErrMsg TypeCheckError
header Maybe SourceSpan
sourceSpan TypeCheckError
footer = do
  Input
input_ <- TypeCheckMonad Input
getInput
  case (Maybe SourceSpan
sourceSpan, Input
input_) of
    (Just SourceSpan
s, Just Vector TypeCheckError
input) ->
          TypeCheckError -> TypeCheckMonad TypeCheckError
forall (m :: * -> *) a. Monad m => a -> m a
return (TypeCheckError -> TypeCheckMonad TypeCheckError)
-> TypeCheckError -> TypeCheckMonad TypeCheckError
forall a b. (a -> b) -> a -> b
$ [TypeCheckError] -> TypeCheckError
forall a. Monoid a => [a] -> a
mconcat [ TypeCheckError
header
                           , TypeCheckError
"\n"
                           , SourceSpan -> Vector TypeCheckError -> TypeCheckError
U.printSourceSpan SourceSpan
s Vector TypeCheckError
input
                           , TypeCheckError
footer
                           ]
    (Maybe SourceSpan, Input)
_                    ->
          TypeCheckError -> TypeCheckMonad TypeCheckError
forall (m :: * -> *) a. Monad m => a -> m a
return (TypeCheckError -> TypeCheckMonad TypeCheckError)
-> TypeCheckError -> TypeCheckMonad TypeCheckError
forall a b. (a -> b) -> a -> b
$ [TypeCheckError] -> TypeCheckError
forall a. Monoid a => [a] -> a
mconcat [ TypeCheckError
header, TypeCheckError
"\n", TypeCheckError
footer ]

-- | Fail with a type-mismatch error.
typeMismatch
    :: Maybe U.SourceSpan
    -> Either Text (Sing (a :: Hakaru))
    -> Either Text (Sing (b :: Hakaru))
    -> TypeCheckMonad r
typeMismatch :: Maybe SourceSpan
-> Either TypeCheckError (Sing a)
-> Either TypeCheckError (Sing b)
-> TypeCheckMonad r
typeMismatch Maybe SourceSpan
s Either TypeCheckError (Sing a)
typ1 Either TypeCheckError (Sing b)
typ2 = TypeCheckError -> TypeCheckMonad r
forall r. TypeCheckError -> TypeCheckMonad r
failwith (TypeCheckError -> TypeCheckMonad r)
-> TypeCheckMonad TypeCheckError -> TypeCheckMonad r
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<
    TypeCheckError
-> Maybe SourceSpan
-> TypeCheckError
-> TypeCheckMonad TypeCheckError
makeErrMsg
     TypeCheckError
"Type Mismatch:"
     Maybe SourceSpan
s
     ([TypeCheckError] -> TypeCheckError
forall a. Monoid a => [a] -> a
mconcat [ TypeCheckError
"expected "
              , TypeCheckError
msg1
              , TypeCheckError
", found "
              , TypeCheckError
msg2
              ])
    where
    msg1 :: TypeCheckError
msg1 = case Either TypeCheckError (Sing a)
typ1 of { Left TypeCheckError
msg -> TypeCheckError
msg; Right Sing a
typ -> Sing a -> TypeCheckError
forall (a :: Hakaru). Sing a -> TypeCheckError
prettyTypeT Sing a
typ }
    msg2 :: TypeCheckError
msg2 = case Either TypeCheckError (Sing b)
typ2 of { Left TypeCheckError
msg -> TypeCheckError
msg; Right Sing b
typ -> Sing b -> TypeCheckError
forall (a :: Hakaru). Sing a -> TypeCheckError
prettyTypeT Sing b
typ }

missingInstance
    :: Text
    -> Sing (a :: Hakaru)
    -> Maybe U.SourceSpan
    -> TypeCheckMonad r
missingInstance :: TypeCheckError -> Sing a -> Maybe SourceSpan -> TypeCheckMonad r
missingInstance TypeCheckError
clas Sing a
typ Maybe SourceSpan
s = TypeCheckError -> TypeCheckMonad r
forall r. TypeCheckError -> TypeCheckMonad r
failwith (TypeCheckError -> TypeCheckMonad r)
-> TypeCheckMonad TypeCheckError -> TypeCheckMonad r
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<
   TypeCheckError
-> Maybe SourceSpan
-> TypeCheckError
-> TypeCheckMonad TypeCheckError
makeErrMsg
    TypeCheckError
"Missing Instance:"
    Maybe SourceSpan
s
    ([TypeCheckError] -> TypeCheckError
forall a. Monoid a => [a] -> a
mconcat ([TypeCheckError] -> TypeCheckError)
-> [TypeCheckError] -> TypeCheckError
forall a b. (a -> b) -> a -> b
$ [TypeCheckError
"No ", TypeCheckError
clas, TypeCheckError
" instance for type ", Sing a -> TypeCheckError
forall (a :: Hakaru). Sing a -> TypeCheckError
prettyTypeT Sing a
typ])

missingLub
    :: Sing (a :: Hakaru)
    -> Sing (b :: Hakaru)
    -> Maybe U.SourceSpan
    -> TypeCheckMonad r
missingLub :: Sing a -> Sing b -> Maybe SourceSpan -> TypeCheckMonad r
missingLub Sing a
typ1 Sing b
typ2 Maybe SourceSpan
s = TypeCheckError -> TypeCheckMonad r
forall r. TypeCheckError -> TypeCheckMonad r
failwith (TypeCheckError -> TypeCheckMonad r)
-> TypeCheckMonad TypeCheckError -> TypeCheckMonad r
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<
    TypeCheckError
-> Maybe SourceSpan
-> TypeCheckError
-> TypeCheckMonad TypeCheckError
makeErrMsg
     TypeCheckError
"Missing common type:"
     Maybe SourceSpan
s
     ([TypeCheckError] -> TypeCheckError
forall a. Monoid a => [a] -> a
mconcat [TypeCheckError
"No lub of types ", Sing a -> TypeCheckError
forall (a :: Hakaru). Sing a -> TypeCheckError
prettyTypeT Sing a
typ1, TypeCheckError
" and ", Sing b -> TypeCheckError
forall (a :: Hakaru). Sing a -> TypeCheckError
prettyTypeT Sing b
typ2])

-- we can't have free variables, so it must be a typo
ambiguousFreeVariable
    :: Text
    -> Maybe U.SourceSpan
    -> TypeCheckMonad r
ambiguousFreeVariable :: TypeCheckError -> Maybe SourceSpan -> TypeCheckMonad r
ambiguousFreeVariable TypeCheckError
x Maybe SourceSpan
s = TypeCheckError -> TypeCheckMonad r
forall r. TypeCheckError -> TypeCheckMonad r
failwith (TypeCheckError -> TypeCheckMonad r)
-> TypeCheckMonad TypeCheckError -> TypeCheckMonad r
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<
    TypeCheckError
-> Maybe SourceSpan
-> TypeCheckError
-> TypeCheckMonad TypeCheckError
makeErrMsg
     ([TypeCheckError] -> TypeCheckError
forall a. Monoid a => [a] -> a
mconcat ([TypeCheckError] -> TypeCheckError)
-> [TypeCheckError] -> TypeCheckError
forall a b. (a -> b) -> a -> b
$ [TypeCheckError
"Name not in scope: ", TypeCheckError
x])
     Maybe SourceSpan
s
     TypeCheckError
"Perhaps it is a typo?"

ambiguousNullCoercion
    :: Maybe U.SourceSpan
    -> TypeCheckMonad r
ambiguousNullCoercion :: Maybe SourceSpan -> TypeCheckMonad r
ambiguousNullCoercion Maybe SourceSpan
s = TypeCheckError -> TypeCheckMonad r
forall r. TypeCheckError -> TypeCheckMonad r
failwith (TypeCheckError -> TypeCheckMonad r)
-> TypeCheckMonad TypeCheckError -> TypeCheckMonad r
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<
    TypeCheckError
-> Maybe SourceSpan
-> TypeCheckError
-> TypeCheckMonad TypeCheckError
makeErrMsg
     TypeCheckError
"Cannot infer type for null-coercion over a checking term."
     Maybe SourceSpan
s
     TypeCheckError
"Please add a type annotation to either the term being coerced or the result of the coercion."

ambiguousEmptyNary
    :: Maybe U.SourceSpan
    -> TypeCheckMonad r
ambiguousEmptyNary :: Maybe SourceSpan -> TypeCheckMonad r
ambiguousEmptyNary Maybe SourceSpan
s = TypeCheckError -> TypeCheckMonad r
forall r. TypeCheckError -> TypeCheckMonad r
failwith (TypeCheckError -> TypeCheckMonad r)
-> TypeCheckMonad TypeCheckError -> TypeCheckMonad r
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<
    TypeCheckError
-> Maybe SourceSpan
-> TypeCheckError
-> TypeCheckMonad TypeCheckError
makeErrMsg
     TypeCheckError
"Cannot infer unambiguous type for empty n-ary operator."
     Maybe SourceSpan
s
     TypeCheckError
"Try adding an annotation on the result of the operator."

ambiguousMustCheckNary
    :: Maybe U.SourceSpan
    -> TypeCheckMonad r
ambiguousMustCheckNary :: Maybe SourceSpan -> TypeCheckMonad r
ambiguousMustCheckNary Maybe SourceSpan
s = TypeCheckError -> TypeCheckMonad r
forall r. TypeCheckError -> TypeCheckMonad r
failwith (TypeCheckError -> TypeCheckMonad r)
-> TypeCheckMonad TypeCheckError -> TypeCheckMonad r
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<
    TypeCheckError
-> Maybe SourceSpan
-> TypeCheckError
-> TypeCheckMonad TypeCheckError
makeErrMsg
     TypeCheckError
"Could not infer any of the arguments."
     Maybe SourceSpan
s
     TypeCheckError
"Try adding a type annotation to at least one of them."

ambiguousMustCheck
    :: Maybe U.SourceSpan
    -> TypeCheckMonad r
ambiguousMustCheck :: Maybe SourceSpan -> TypeCheckMonad r
ambiguousMustCheck Maybe SourceSpan
s = TypeCheckError -> TypeCheckMonad r
forall r. TypeCheckError -> TypeCheckMonad r
failwith (TypeCheckError -> TypeCheckMonad r)
-> TypeCheckMonad TypeCheckError -> TypeCheckMonad r
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<
    TypeCheckError
-> Maybe SourceSpan
-> TypeCheckError
-> TypeCheckMonad TypeCheckError
makeErrMsg
     TypeCheckError
"Cannot infer types for checking terms."
     Maybe SourceSpan
s
     TypeCheckError
"Please add a type annotation."

argumentNumberError
     :: TypeCheckMonad r
argumentNumberError :: TypeCheckMonad r
argumentNumberError = TypeCheckError -> TypeCheckMonad r
forall r. TypeCheckError -> TypeCheckMonad r
failwith (TypeCheckError -> TypeCheckMonad r)
-> TypeCheckMonad TypeCheckError -> TypeCheckMonad r
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<
    TypeCheckError
-> Maybe SourceSpan
-> TypeCheckError
-> TypeCheckMonad TypeCheckError
makeErrMsg TypeCheckError
"Argument error:" Maybe SourceSpan
forall a. Maybe a
Nothing TypeCheckError
"Passed wrong number of arguments"

-- | * Terms whose type is existentially quantified packed with a singleton for
-- the type.

-- BUG: haddock doesn't like annotations on GADT constructors. So
-- here we'll avoid using the GADT syntax, even though it'd make
-- the data type declaration prettier\/cleaner.
-- <https://github.com/hakaru-dev/hakaru/issues/6>
--
-- | The @e' ∈ τ@ portion of the inference judgement.
data TypedAST (abt :: [Hakaru] -> Hakaru -> *)
    = forall b. TypedAST !(Sing b) !(abt '[] b)

onTypedAST :: (forall b . abt '[] b -> abt '[] b) -> TypedAST abt -> TypedAST abt
onTypedAST :: (forall (b :: Hakaru). abt '[] b -> abt '[] b)
-> TypedAST abt -> TypedAST abt
onTypedAST forall (b :: Hakaru). abt '[] b -> abt '[] b
f (TypedAST Sing b
t abt '[] b
p) = Sing b -> abt '[] b -> TypedAST abt
forall (abt :: [Hakaru] -> Hakaru -> *) (b :: Hakaru).
Sing b -> abt '[] b -> TypedAST abt
TypedAST Sing b
t (abt '[] b -> abt '[] b
forall (b :: Hakaru). abt '[] b -> abt '[] b
f abt '[] b
p)

onTypedASTM :: (Functor m)
            => (forall b . abt '[] b -> m (abt '[] b))
            -> TypedAST abt -> m (TypedAST abt)
onTypedASTM :: (forall (b :: Hakaru). abt '[] b -> m (abt '[] b))
-> TypedAST abt -> m (TypedAST abt)
onTypedASTM forall (b :: Hakaru). abt '[] b -> m (abt '[] b)
f (TypedAST Sing b
t abt '[] b
p) = Sing b -> abt '[] b -> TypedAST abt
forall (abt :: [Hakaru] -> Hakaru -> *) (b :: Hakaru).
Sing b -> abt '[] b -> TypedAST abt
TypedAST Sing b
t (abt '[] b -> TypedAST abt) -> m (abt '[] b) -> m (TypedAST abt)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> abt '[] b -> m (abt '[] b)
forall (b :: Hakaru). abt '[] b -> m (abt '[] b)
f abt '[] b
p

elimTypedAST :: (forall b . Sing b -> abt '[] b -> x) -> TypedAST abt -> x 
elimTypedAST :: (forall (b :: Hakaru). Sing b -> abt '[] b -> x)
-> TypedAST abt -> x
elimTypedAST forall (b :: Hakaru). Sing b -> abt '[] b -> x
f (TypedAST Sing b
t abt '[] b
p) = Sing b -> abt '[] b -> x
forall (b :: Hakaru). Sing b -> abt '[] b -> x
f Sing b
t abt '[] b
p 

instance Show2 abt => Show (TypedAST abt) where
    showsPrec :: Int -> TypedAST abt -> ShowS
showsPrec Int
p (TypedAST Sing b
typ abt '[] b
e) =
        Int -> String -> Sing b -> abt '[] b -> ShowS
forall k k1 k2 (a :: k -> *) (b :: k1 -> k2 -> *) (i :: k)
       (j :: k1) (l :: k2).
(Show1 a, Show2 b) =>
Int -> String -> a i -> b j l -> ShowS
showParen_12 Int
p String
"TypedAST" Sing b
typ abt '[] b
e


----------------------------------------------------------------
data TypedASTs (abt :: [Hakaru] -> Hakaru -> *)
    = forall b. TypedASTs !(Sing b) [abt '[] b]

{-
instance Show2 abt => Show (TypedASTs abt) where
    showsPrec p (TypedASTs typ es) =
        showParen_1x p "TypedASTs" typ es
-}

----------------------------------------------------------------
-- HACK: Passing this list of variables feels like a hack
-- it would be nice if it could be removed from this datatype
data TypedReducer (abt :: [Hakaru] -> Hakaru -> *)
                  (xs  :: [Hakaru])
    = forall b. TypedReducer !(Sing b) (List1 Variable xs) (Reducer abt xs b)

----------------------------------------------------------------
-- BUG: haddock doesn't like annotations on GADT constructors. So
-- here we'll avoid using the GADT syntax, even though it'd make
-- the data type declaration prettier\/cleaner.
-- <https://github.com/hakaru-dev/hakaru/issues/6>
data SomePattern (a :: Hakaru) =
    forall vars.
        SP  !(Pattern vars a)
            !(List1 Variable vars)

data SomePatternCode xss t =
    forall vars.
        SPC !(PDatumCode xss vars (HData' t))
            !(List1 Variable vars)

data SomePatternStruct xs t =
    forall vars.
        SPS !(PDatumStruct xs vars (HData' t))
            !(List1 Variable vars)

data SomePatternFun x t =
    forall vars.
        SPF !(PDatumFun x vars (HData' t))
            !(List1 Variable vars)

data SomeBranch a abt = forall b. SomeBranch !(Sing b) [Branch a abt b]

-- | * Misc.

makeVar :: forall (a :: Hakaru). Variable 'U.U -> Sing a -> Variable a
makeVar :: Variable 'U -> Sing a -> Variable a
makeVar (Variable TypeCheckError
hintID Nat
nameID Sing 'U
_) Sing a
typ =
    TypeCheckError -> Nat -> Sing a -> Variable a
forall k (a :: k). TypeCheckError -> Nat -> Sing a -> Variable a
Variable TypeCheckError
hintID Nat
nameID Sing a
typ

make_NaryOp :: Sing a -> U.NaryOp -> TypeCheckMonad (NaryOp a)
make_NaryOp :: Sing a -> NaryOp -> TypeCheckMonad (NaryOp a)
make_NaryOp Sing a
a NaryOp
U.And  = Sing a -> TypeCheckMonad (TypeEq a HBool)
forall (a :: Hakaru). Sing a -> TypeCheckMonad (TypeEq a HBool)
isBool Sing a
a TypeCheckMonad (TypeEq a HBool)
-> (TypeEq a HBool -> TypeCheckMonad (NaryOp a))
-> TypeCheckMonad (NaryOp a)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \TypeEq a HBool
Refl -> NaryOp HBool -> TypeCheckMonad (NaryOp HBool)
forall (m :: * -> *) a. Monad m => a -> m a
return NaryOp HBool
And
make_NaryOp Sing a
a NaryOp
U.Or   = Sing a -> TypeCheckMonad (TypeEq a HBool)
forall (a :: Hakaru). Sing a -> TypeCheckMonad (TypeEq a HBool)
isBool Sing a
a TypeCheckMonad (TypeEq a HBool)
-> (TypeEq a HBool -> TypeCheckMonad (NaryOp a))
-> TypeCheckMonad (NaryOp a)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \TypeEq a HBool
Refl -> NaryOp HBool -> TypeCheckMonad (NaryOp HBool)
forall (m :: * -> *) a. Monad m => a -> m a
return NaryOp HBool
Or
make_NaryOp Sing a
a NaryOp
U.Xor  = Sing a -> TypeCheckMonad (TypeEq a HBool)
forall (a :: Hakaru). Sing a -> TypeCheckMonad (TypeEq a HBool)
isBool Sing a
a TypeCheckMonad (TypeEq a HBool)
-> (TypeEq a HBool -> TypeCheckMonad (NaryOp a))
-> TypeCheckMonad (NaryOp a)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \TypeEq a HBool
Refl -> NaryOp HBool -> TypeCheckMonad (NaryOp HBool)
forall (m :: * -> *) a. Monad m => a -> m a
return NaryOp HBool
Xor
make_NaryOp Sing a
a NaryOp
U.Iff  = Sing a -> TypeCheckMonad (TypeEq a HBool)
forall (a :: Hakaru). Sing a -> TypeCheckMonad (TypeEq a HBool)
isBool Sing a
a TypeCheckMonad (TypeEq a HBool)
-> (TypeEq a HBool -> TypeCheckMonad (NaryOp a))
-> TypeCheckMonad (NaryOp a)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \TypeEq a HBool
Refl -> NaryOp HBool -> TypeCheckMonad (NaryOp HBool)
forall (m :: * -> *) a. Monad m => a -> m a
return NaryOp HBool
Iff
make_NaryOp Sing a
a NaryOp
U.Min  = HOrd a -> NaryOp a
forall (a :: Hakaru). HOrd a -> NaryOp a
Min  (HOrd a -> NaryOp a)
-> TypeCheckMonad (HOrd a) -> TypeCheckMonad (NaryOp a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Sing a -> TypeCheckMonad (HOrd a)
forall (a :: Hakaru). Sing a -> TypeCheckMonad (HOrd a)
getHOrd Sing a
a
make_NaryOp Sing a
a NaryOp
U.Max  = HOrd a -> NaryOp a
forall (a :: Hakaru). HOrd a -> NaryOp a
Max  (HOrd a -> NaryOp a)
-> TypeCheckMonad (HOrd a) -> TypeCheckMonad (NaryOp a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Sing a -> TypeCheckMonad (HOrd a)
forall (a :: Hakaru). Sing a -> TypeCheckMonad (HOrd a)
getHOrd Sing a
a
make_NaryOp Sing a
a NaryOp
U.Sum  = HSemiring a -> NaryOp a
forall (a :: Hakaru). HSemiring a -> NaryOp a
Sum  (HSemiring a -> NaryOp a)
-> TypeCheckMonad (HSemiring a) -> TypeCheckMonad (NaryOp a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Sing a -> TypeCheckMonad (HSemiring a)
forall (a :: Hakaru). Sing a -> TypeCheckMonad (HSemiring a)
getHSemiring Sing a
a
make_NaryOp Sing a
a NaryOp
U.Prod = HSemiring a -> NaryOp a
forall (a :: Hakaru). HSemiring a -> NaryOp a
Prod (HSemiring a -> NaryOp a)
-> TypeCheckMonad (HSemiring a) -> TypeCheckMonad (NaryOp a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Sing a -> TypeCheckMonad (HSemiring a)
forall (a :: Hakaru). Sing a -> TypeCheckMonad (HSemiring a)
getHSemiring Sing a
a

isBool :: Sing a -> TypeCheckMonad (TypeEq a HBool)
isBool :: Sing a -> TypeCheckMonad (TypeEq a HBool)
isBool Sing a
typ =
    case Sing a -> Sing HBool -> Maybe (TypeEq a HBool)
forall k (a :: k -> *) (i :: k) (j :: k).
JmEq1 a =>
a i -> a j -> Maybe (TypeEq i j)
jmEq1 Sing a
typ Sing HBool
sBool of
    Just TypeEq a HBool
proof -> TypeEq a HBool -> TypeCheckMonad (TypeEq a HBool)
forall (m :: * -> *) a. Monad m => a -> m a
return TypeEq a HBool
proof
    Maybe (TypeEq a HBool)
Nothing    -> Maybe SourceSpan
-> Either TypeCheckError (Sing Any)
-> Either TypeCheckError (Sing a)
-> TypeCheckMonad (TypeEq a HBool)
forall (a :: Hakaru) (b :: Hakaru) r.
Maybe SourceSpan
-> Either TypeCheckError (Sing a)
-> Either TypeCheckError (Sing b)
-> TypeCheckMonad r
typeMismatch Maybe SourceSpan
forall a. Maybe a
Nothing (TypeCheckError -> Either TypeCheckError (Sing Any)
forall a b. a -> Either a b
Left TypeCheckError
"HBool") (Sing a -> Either TypeCheckError (Sing a)
forall a b. b -> Either a b
Right Sing a
typ)


jmEq1_ :: Sing (a :: Hakaru)
       -> Sing (b :: Hakaru)
       -> TypeCheckMonad (TypeEq a b)
jmEq1_ :: Sing a -> Sing b -> TypeCheckMonad (TypeEq a b)
jmEq1_ Sing a
typA Sing b
typB =
    case Sing a -> Sing b -> Maybe (TypeEq a b)
forall k (a :: k -> *) (i :: k) (j :: k).
JmEq1 a =>
a i -> a j -> Maybe (TypeEq i j)
jmEq1 Sing a
typA Sing b
typB of
    Just TypeEq a b
proof -> TypeEq a b -> TypeCheckMonad (TypeEq a b)
forall (m :: * -> *) a. Monad m => a -> m a
return TypeEq a b
proof
    Maybe (TypeEq a b)
Nothing    -> Maybe SourceSpan
-> Either TypeCheckError (Sing a)
-> Either TypeCheckError (Sing b)
-> TypeCheckMonad (TypeEq a b)
forall (a :: Hakaru) (b :: Hakaru) r.
Maybe SourceSpan
-> Either TypeCheckError (Sing a)
-> Either TypeCheckError (Sing b)
-> TypeCheckMonad r
typeMismatch Maybe SourceSpan
forall a. Maybe a
Nothing (Sing a -> Either TypeCheckError (Sing a)
forall a b. b -> Either a b
Right Sing a
typA) (Sing b -> Either TypeCheckError (Sing b)
forall a b. b -> Either a b
Right Sing b
typB)


getHEq :: Sing a -> TypeCheckMonad (HEq a)
getHEq :: Sing a -> TypeCheckMonad (HEq a)
getHEq Sing a
typ =
    case Sing a -> Maybe (HEq a)
forall (a :: Hakaru). Sing a -> Maybe (HEq a)
hEq_Sing Sing a
typ of
    Just HEq a
theEq -> HEq a -> TypeCheckMonad (HEq a)
forall (m :: * -> *) a. Monad m => a -> m a
return HEq a
theEq
    Maybe (HEq a)
Nothing    -> TypeCheckError
-> Sing a -> Maybe SourceSpan -> TypeCheckMonad (HEq a)
forall (a :: Hakaru) r.
TypeCheckError -> Sing a -> Maybe SourceSpan -> TypeCheckMonad r
missingInstance TypeCheckError
"HEq" Sing a
typ Maybe SourceSpan
forall a. Maybe a
Nothing

getHOrd :: Sing a -> TypeCheckMonad (HOrd a)
getHOrd :: Sing a -> TypeCheckMonad (HOrd a)
getHOrd Sing a
typ =
    case Sing a -> Maybe (HOrd a)
forall (a :: Hakaru). Sing a -> Maybe (HOrd a)
hOrd_Sing Sing a
typ of
    Just HOrd a
theOrd -> HOrd a -> TypeCheckMonad (HOrd a)
forall (m :: * -> *) a. Monad m => a -> m a
return HOrd a
theOrd
    Maybe (HOrd a)
Nothing     -> TypeCheckError
-> Sing a -> Maybe SourceSpan -> TypeCheckMonad (HOrd a)
forall (a :: Hakaru) r.
TypeCheckError -> Sing a -> Maybe SourceSpan -> TypeCheckMonad r
missingInstance TypeCheckError
"HOrd" Sing a
typ Maybe SourceSpan
forall a. Maybe a
Nothing

getHSemiring :: Sing a -> TypeCheckMonad (HSemiring a)
getHSemiring :: Sing a -> TypeCheckMonad (HSemiring a)
getHSemiring Sing a
typ =
    case Sing a -> Maybe (HSemiring a)
forall (a :: Hakaru). Sing a -> Maybe (HSemiring a)
hSemiring_Sing Sing a
typ of
    Just HSemiring a
theSemi -> HSemiring a -> TypeCheckMonad (HSemiring a)
forall (m :: * -> *) a. Monad m => a -> m a
return HSemiring a
theSemi
    Maybe (HSemiring a)
Nothing      -> TypeCheckError
-> Sing a -> Maybe SourceSpan -> TypeCheckMonad (HSemiring a)
forall (a :: Hakaru) r.
TypeCheckError -> Sing a -> Maybe SourceSpan -> TypeCheckMonad r
missingInstance TypeCheckError
"HSemiring" Sing a
typ Maybe SourceSpan
forall a. Maybe a
Nothing

getHRing :: Sing a -> TypeCheckMode -> TypeCheckMonad (SomeRing a)
getHRing :: Sing a -> TypeCheckMode -> TypeCheckMonad (SomeRing a)
getHRing Sing a
typ TypeCheckMode
mode =
    case TypeCheckMode
mode of
    TypeCheckMode
StrictMode -> case Sing a -> Maybe (HRing a)
forall (a :: Hakaru). Sing a -> Maybe (HRing a)
hRing_Sing Sing a
typ of
                    Just HRing a
theRing -> SomeRing a -> TypeCheckMonad (SomeRing a)
forall (m :: * -> *) a. Monad m => a -> m a
return (HRing a -> Coercion a a -> SomeRing a
forall (a :: Hakaru) (b :: Hakaru).
HRing b -> Coercion a b -> SomeRing a
SomeRing HRing a
theRing Coercion a a
forall (a :: Hakaru). Coercion a a
CNil)
                    Maybe (HRing a)
Nothing      -> TypeCheckError
-> Sing a -> Maybe SourceSpan -> TypeCheckMonad (SomeRing a)
forall (a :: Hakaru) r.
TypeCheckError -> Sing a -> Maybe SourceSpan -> TypeCheckMonad r
missingInstance TypeCheckError
"HRing" Sing a
typ Maybe SourceSpan
forall a. Maybe a
Nothing
    TypeCheckMode
LaxMode    -> case Sing a -> Maybe (SomeRing a)
forall (a :: Hakaru). Sing a -> Maybe (SomeRing a)
findRing Sing a
typ of
                    Just SomeRing a
proof   -> SomeRing a -> TypeCheckMonad (SomeRing a)
forall (m :: * -> *) a. Monad m => a -> m a
return SomeRing a
proof
                    Maybe (SomeRing a)
Nothing      -> TypeCheckError
-> Sing a -> Maybe SourceSpan -> TypeCheckMonad (SomeRing a)
forall (a :: Hakaru) r.
TypeCheckError -> Sing a -> Maybe SourceSpan -> TypeCheckMonad r
missingInstance TypeCheckError
"HRing" Sing a
typ Maybe SourceSpan
forall a. Maybe a
Nothing
    TypeCheckMode
UnsafeMode -> case Sing a -> Maybe (SomeRing a)
forall (a :: Hakaru). Sing a -> Maybe (SomeRing a)
findRing Sing a
typ of
                    Just SomeRing a
proof   -> SomeRing a -> TypeCheckMonad (SomeRing a)
forall (m :: * -> *) a. Monad m => a -> m a
return SomeRing a
proof
                    Maybe (SomeRing a)
Nothing      -> TypeCheckError
-> Sing a -> Maybe SourceSpan -> TypeCheckMonad (SomeRing a)
forall (a :: Hakaru) r.
TypeCheckError -> Sing a -> Maybe SourceSpan -> TypeCheckMonad r
missingInstance TypeCheckError
"HRing" Sing a
typ Maybe SourceSpan
forall a. Maybe a
Nothing

getHFractional :: Sing a -> TypeCheckMode -> TypeCheckMonad (SomeFractional a)
getHFractional :: Sing a -> TypeCheckMode -> TypeCheckMonad (SomeFractional a)
getHFractional Sing a
typ TypeCheckMode
mode =
    case TypeCheckMode
mode of
    TypeCheckMode
StrictMode -> case Sing a -> Maybe (HFractional a)
forall (a :: Hakaru). Sing a -> Maybe (HFractional a)
hFractional_Sing Sing a
typ of
                    Just HFractional a
theFrac -> SomeFractional a -> TypeCheckMonad (SomeFractional a)
forall (m :: * -> *) a. Monad m => a -> m a
return (HFractional a -> Coercion a a -> SomeFractional a
forall (a :: Hakaru) (b :: Hakaru).
HFractional b -> Coercion a b -> SomeFractional a
SomeFractional HFractional a
theFrac Coercion a a
forall (a :: Hakaru). Coercion a a
CNil)
                    Maybe (HFractional a)
Nothing      -> TypeCheckError
-> Sing a -> Maybe SourceSpan -> TypeCheckMonad (SomeFractional a)
forall (a :: Hakaru) r.
TypeCheckError -> Sing a -> Maybe SourceSpan -> TypeCheckMonad r
missingInstance TypeCheckError
"HFractional" Sing a
typ Maybe SourceSpan
forall a. Maybe a
Nothing
    TypeCheckMode
LaxMode    -> case Sing a -> Maybe (SomeFractional a)
forall (a :: Hakaru). Sing a -> Maybe (SomeFractional a)
findFractional Sing a
typ of
                    Just SomeFractional a
proof   -> SomeFractional a -> TypeCheckMonad (SomeFractional a)
forall (m :: * -> *) a. Monad m => a -> m a
return SomeFractional a
proof
                    Maybe (SomeFractional a)
Nothing      -> TypeCheckError
-> Sing a -> Maybe SourceSpan -> TypeCheckMonad (SomeFractional a)
forall (a :: Hakaru) r.
TypeCheckError -> Sing a -> Maybe SourceSpan -> TypeCheckMonad r
missingInstance TypeCheckError
"HFractional" Sing a
typ Maybe SourceSpan
forall a. Maybe a
Nothing
    TypeCheckMode
UnsafeMode -> case Sing a -> Maybe (SomeFractional a)
forall (a :: Hakaru). Sing a -> Maybe (SomeFractional a)
findFractional Sing a
typ of
                    Just SomeFractional a
proof   -> SomeFractional a -> TypeCheckMonad (SomeFractional a)
forall (m :: * -> *) a. Monad m => a -> m a
return SomeFractional a
proof
                    Maybe (SomeFractional a)
Nothing      -> TypeCheckError
-> Sing a -> Maybe SourceSpan -> TypeCheckMonad (SomeFractional a)
forall (a :: Hakaru) r.
TypeCheckError -> Sing a -> Maybe SourceSpan -> TypeCheckMonad r
missingInstance TypeCheckError
"HFractional" Sing a
typ Maybe SourceSpan
forall a. Maybe a
Nothing

-- TODO: find a better name, and move to where 'LC_' is defined.
lc :: (LC_ abt a -> LC_ abt b) -> abt '[] a -> abt '[] b
lc :: (LC_ abt a -> LC_ abt b) -> abt '[] a -> abt '[] b
lc LC_ abt a -> LC_ abt b
f = LC_ abt b -> abt '[] b
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
LC_ abt a -> abt '[] a
unLC_ (LC_ abt b -> abt '[] b)
-> (abt '[] a -> LC_ abt b) -> abt '[] a -> abt '[] b
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. LC_ abt a -> LC_ abt b
f (LC_ abt a -> LC_ abt b)
-> (abt '[] a -> LC_ abt a) -> abt '[] a -> LC_ abt b
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. abt '[] a -> LC_ abt a
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
abt '[] a -> LC_ abt a
LC_

coerceTo_nonLC :: (ABT Term abt) => Coercion a b -> abt xs a -> abt xs b
coerceTo_nonLC :: Coercion a b -> abt xs a -> abt xs b
coerceTo_nonLC = (abt '[] a -> abt '[] b) -> abt xs a -> abt xs b
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k) (b :: k) (xs :: [k]).
ABT syn abt =>
(abt '[] a -> abt '[] b) -> abt xs a -> abt xs b
underBinders ((abt '[] a -> abt '[] b) -> abt xs a -> abt xs b)
-> (Coercion a b -> abt '[] a -> abt '[] b)
-> Coercion a b
-> abt xs a
-> abt xs b
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (LC_ abt a -> LC_ abt b) -> abt '[] a -> abt '[] b
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
       (b :: Hakaru).
(LC_ abt a -> LC_ abt b) -> abt '[] a -> abt '[] b
lc ((LC_ abt a -> LC_ abt b) -> abt '[] a -> abt '[] b)
-> (Coercion a b -> LC_ abt a -> LC_ abt b)
-> Coercion a b
-> abt '[] a
-> abt '[] b
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Coercion a b -> LC_ abt a -> LC_ abt b
forall (f :: Hakaru -> *) (a :: Hakaru) (b :: Hakaru).
Coerce f =>
Coercion a b -> f a -> f b
coerceTo

coerceFrom_nonLC :: (ABT Term abt) => Coercion a b -> abt xs b -> abt xs a
coerceFrom_nonLC :: Coercion a b -> abt xs b -> abt xs a
coerceFrom_nonLC = (abt '[] b -> abt '[] a) -> abt xs b -> abt xs a
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k) (b :: k) (xs :: [k]).
ABT syn abt =>
(abt '[] a -> abt '[] b) -> abt xs a -> abt xs b
underBinders ((abt '[] b -> abt '[] a) -> abt xs b -> abt xs a)
-> (Coercion a b -> abt '[] b -> abt '[] a)
-> Coercion a b
-> abt xs b
-> abt xs a
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (LC_ abt b -> LC_ abt a) -> abt '[] b -> abt '[] a
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
       (b :: Hakaru).
(LC_ abt a -> LC_ abt b) -> abt '[] a -> abt '[] b
lc ((LC_ abt b -> LC_ abt a) -> abt '[] b -> abt '[] a)
-> (Coercion a b -> LC_ abt b -> LC_ abt a)
-> Coercion a b
-> abt '[] b
-> abt '[] a
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Coercion a b -> LC_ abt b -> LC_ abt a
forall (f :: Hakaru -> *) (a :: Hakaru) (b :: Hakaru).
Coerce f =>
Coercion a b -> f b -> f a
coerceFrom

-- BUG: how to make this not an orphan, without dealing with cyclic imports between AST.hs (for the 'LC_' instance), Datum.hs, and Coercion.hs?
instance (ABT Term abt) => Coerce (Branch a abt) where
    coerceTo :: Coercion a b -> Branch a abt a -> Branch a abt b
coerceTo   Coercion a b
c (Branch Pattern xs a
pat abt xs a
e) = Pattern xs a -> abt xs b -> Branch a abt b
forall (a :: Hakaru) (abt :: [Hakaru] -> Hakaru -> *) (b :: Hakaru)
       (xs :: [Hakaru]).
Pattern xs a -> abt xs b -> Branch a abt b
Branch Pattern xs a
pat (Coercion a b -> abt xs a -> abt xs b
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru) (b :: Hakaru)
       (xs :: [Hakaru]).
ABT Term abt =>
Coercion a b -> abt xs a -> abt xs b
coerceTo_nonLC   Coercion a b
c abt xs a
e)
    coerceFrom :: Coercion a b -> Branch a abt b -> Branch a abt a
coerceFrom Coercion a b
c (Branch Pattern xs a
pat abt xs b
e) = Pattern xs a -> abt xs a -> Branch a abt a
forall (a :: Hakaru) (abt :: [Hakaru] -> Hakaru -> *) (b :: Hakaru)
       (xs :: [Hakaru]).
Pattern xs a -> abt xs b -> Branch a abt b
Branch Pattern xs a
pat (Coercion a b -> abt xs b -> abt xs a
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru) (b :: Hakaru)
       (xs :: [Hakaru]).
ABT Term abt =>
Coercion a b -> abt xs b -> abt xs a
coerceFrom_nonLC Coercion a b
c abt xs b
e)