{-# LANGUAGE CPP
, ScopedTypeVariables
, GADTs
, DataKinds
, KindSignatures
, GeneralizedNewtypeDeriving
, TypeOperators
, FlexibleContexts
, FlexibleInstances
, OverloadedStrings
, PatternGuards
, Rank2Types
#-}
{-# OPTIONS_GHC -Wall -fwarn-tabs #-}
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)
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
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
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
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
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
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
Right a
e -> a -> Maybe a
forall a. a -> Maybe a
Just a
e
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
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 ]
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])
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"
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]
data TypedReducer (abt :: [Hakaru] -> Hakaru -> *)
(xs :: [Hakaru])
= forall b. TypedReducer !(Sing b) (List1 Variable xs) (Reducer abt xs b)
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]
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
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
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)