{-# LANGUAGE CPP
, ScopedTypeVariables
, GADTs
, DataKinds
, KindSignatures
, GeneralizedNewtypeDeriving
, TypeOperators
, FlexibleContexts
, FlexibleInstances
, OverloadedStrings
, PatternGuards
, Rank2Types
, LiberalTypeSynonyms
#-}
{-# OPTIONS_GHC -Wall -fwarn-tabs #-}
module Language.Hakaru.Syntax.TypeCheck.Unification where
import Language.Hakaru.Syntax.TypeCheck.TypeCheckMonad
import Language.Hakaru.Types.DataKind (Hakaru(..), HPair)
import Language.Hakaru.Types.Sing
import Language.Hakaru.Syntax.IClasses
import qualified Language.Hakaru.Parser.AST as U
import Data.Text (Text)
type Metadata = Maybe U.SourceSpan
type Unify1 (t :: Hakaru -> Hakaru) r x
= Sing x
-> Metadata
-> (forall a . x ~ t a => Sing a -> TypeCheckMonad r)
-> TypeCheckMonad r
type Unify2 (t :: Hakaru -> Hakaru -> Hakaru) r x
= Sing x
-> Metadata
-> (forall a b . x ~ t a b => Sing a -> Sing b -> TypeCheckMonad r)
-> TypeCheckMonad r
class TCMTypeRepr x where
toTypeRepr :: x -> Maybe (Either Text (Some1 (Sing :: Hakaru -> *)))
instance TCMTypeRepr (Sing (x :: Hakaru)) where
toTypeRepr :: Sing x -> Maybe (Either Text (Some1 Sing))
toTypeRepr = Either Text (Some1 Sing) -> Maybe (Either Text (Some1 Sing))
forall a. a -> Maybe a
Just (Either Text (Some1 Sing) -> Maybe (Either Text (Some1 Sing)))
-> (Sing x -> Either Text (Some1 Sing))
-> Sing x
-> Maybe (Either Text (Some1 Sing))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Some1 Sing -> Either Text (Some1 Sing)
forall a b. b -> Either a b
Right (Some1 Sing -> Either Text (Some1 Sing))
-> (Sing x -> Some1 Sing) -> Sing x -> Either Text (Some1 Sing)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sing x -> Some1 Sing
forall k (a :: k -> *) (i :: k). a i -> Some1 a
Some1
instance TCMTypeRepr Text where
toTypeRepr :: Text -> Maybe (Either Text (Some1 Sing))
toTypeRepr = Either Text (Some1 Sing) -> Maybe (Either Text (Some1 Sing))
forall a. a -> Maybe a
Just (Either Text (Some1 Sing) -> Maybe (Either Text (Some1 Sing)))
-> (Text -> Either Text (Some1 Sing))
-> Text
-> Maybe (Either Text (Some1 Sing))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> Either Text (Some1 Sing)
forall a b. a -> Either a b
Left
instance TCMTypeRepr () where
toTypeRepr :: () -> Maybe (Either Text (Some1 Sing))
toTypeRepr () = Maybe (Either Text (Some1 Sing))
forall a. Maybe a
Nothing
unifyMeasure :: Unify1 'HMeasure r x
unifyMeasure :: Unify1 'HMeasure r x
unifyMeasure Sing x
ty Metadata
m forall (a :: Hakaru).
(x ~ 'HMeasure a) =>
Sing a -> TypeCheckMonad r
k =
case Sing x
ty of
SMeasure a -> Sing a -> TypeCheckMonad r
forall (a :: Hakaru).
(x ~ 'HMeasure a) =>
Sing a -> TypeCheckMonad r
k Sing a
a
Sing x
_ -> Metadata
-> Either Text (Sing Any)
-> Either Text (Sing x)
-> TypeCheckMonad r
forall (a :: Hakaru) (b :: Hakaru) r.
Metadata
-> Either Text (Sing a) -> Either Text (Sing b) -> TypeCheckMonad r
typeMismatch Metadata
m (Text -> Either Text (Sing Any)
forall a b. a -> Either a b
Left Text
"HMeasure") (Sing x -> Either Text (Sing x)
forall a b. b -> Either a b
Right Sing x
ty)
unifyArray :: Unify1 'HArray r x
unifyArray :: Unify1 'HArray r x
unifyArray Sing x
ty Metadata
m forall (a :: Hakaru). (x ~ 'HArray a) => Sing a -> TypeCheckMonad r
k =
case Sing x
ty of
SArray a -> Sing a -> TypeCheckMonad r
forall (a :: Hakaru). (x ~ 'HArray a) => Sing a -> TypeCheckMonad r
k Sing a
a
Sing x
_ -> Metadata
-> Either Text (Sing Any)
-> Either Text (Sing x)
-> TypeCheckMonad r
forall (a :: Hakaru) (b :: Hakaru) r.
Metadata
-> Either Text (Sing a) -> Either Text (Sing b) -> TypeCheckMonad r
typeMismatch Metadata
m (Text -> Either Text (Sing Any)
forall a b. a -> Either a b
Left Text
"HArray") (Sing x -> Either Text (Sing x)
forall a b. b -> Either a b
Right Sing x
ty)
unifyFun :: Unify2 '(:->) r x
unifyFun :: Unify2 (':->) r x
unifyFun Sing x
ty Metadata
m forall (a :: Hakaru) (b :: Hakaru).
(x ~ (a ':-> b)) =>
Sing a -> Sing b -> TypeCheckMonad r
k =
case Sing x
ty of
SFun a b -> Sing a -> Sing b -> TypeCheckMonad r
forall (a :: Hakaru) (b :: Hakaru).
(x ~ (a ':-> b)) =>
Sing a -> Sing b -> TypeCheckMonad r
k Sing a
a Sing b
b
Sing x
_ -> Metadata
-> Either Text (Sing Any)
-> Either Text (Sing x)
-> TypeCheckMonad r
forall (a :: Hakaru) (b :: Hakaru) r.
Metadata
-> Either Text (Sing a) -> Either Text (Sing b) -> TypeCheckMonad r
typeMismatch Metadata
m (Text -> Either Text (Sing Any)
forall a b. a -> Either a b
Left Text
":->") (Sing x -> Either Text (Sing x)
forall a b. b -> Either a b
Right Sing x
ty)
unifyPair :: Unify2 HPair r x
unifyPair :: Unify2 HPair r x
unifyPair Sing x
ty Metadata
m forall (a :: Hakaru) (b :: Hakaru).
(x ~ HPair a b) =>
Sing a -> Sing b -> TypeCheckMonad r
k =
TypeCheckMonad r
-> (TypeCheckMonad r -> TypeCheckMonad r)
-> Maybe (TypeCheckMonad r)
-> TypeCheckMonad r
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Metadata
-> Either Text (Sing Any)
-> Either Text (Sing x)
-> TypeCheckMonad r
forall (a :: Hakaru) (b :: Hakaru) r.
Metadata
-> Either Text (Sing a) -> Either Text (Sing b) -> TypeCheckMonad r
typeMismatch Metadata
m (Text -> Either Text (Sing Any)
forall a b. a -> Either a b
Left Text
"HPair") (Sing x -> Either Text (Sing x)
forall a b. b -> Either a b
Right Sing x
ty)) TypeCheckMonad r -> TypeCheckMonad r
forall a. a -> a
id (Maybe (TypeCheckMonad r) -> TypeCheckMonad r)
-> Maybe (TypeCheckMonad r) -> TypeCheckMonad r
forall a b. (a -> b) -> a -> b
$ do
SData (STyCon sym `STyApp` a `STyApp` b) _ <- Sing x -> Maybe (Sing x)
forall a. a -> Maybe a
Just Sing x
ty
TypeEq s "Pair"
Refl <- Sing s -> Sing "Pair" -> Maybe (TypeEq s "Pair")
forall k (a :: k -> *) (i :: k) (j :: k).
JmEq1 a =>
a i -> a j -> Maybe (TypeEq i j)
jmEq1 Sing s
sym Sing "Pair"
sSymbol_Pair
TypeCheckMonad r -> Maybe (TypeCheckMonad r)
forall a. a -> Maybe a
Just (TypeCheckMonad r -> Maybe (TypeCheckMonad r))
-> TypeCheckMonad r -> Maybe (TypeCheckMonad r)
forall a b. (a -> b) -> a -> b
$ Sing b -> Sing b -> TypeCheckMonad r
forall (a :: Hakaru) (b :: Hakaru).
(x ~ HPair a b) =>
Sing a -> Sing b -> TypeCheckMonad r
k Sing b
a Sing b
b
matchTypes
:: (TCMTypeRepr t0, TCMTypeRepr t1)
=> Sing (x :: Hakaru)
-> Sing y
-> Metadata
-> t0 -> t1
-> (x ~ y => TypeCheckMonad r)
-> TypeCheckMonad r
matchTypes :: Sing x
-> Sing y
-> Metadata
-> t0
-> t1
-> ((x ~ y) => TypeCheckMonad r)
-> TypeCheckMonad r
matchTypes Sing x
t0 Sing y
t1 Metadata
m t0
e0 t1
e1 (x ~ y) => TypeCheckMonad r
k
| Just TypeEq x y
Refl <- Sing x -> Sing y -> Maybe (TypeEq x y)
forall k (a :: k -> *) (i :: k) (j :: k).
JmEq1 a =>
a i -> a j -> Maybe (TypeEq i j)
jmEq1 Sing x
t0 Sing y
t1 = TypeCheckMonad r
(x ~ y) => TypeCheckMonad r
k
| Bool
otherwise =
let tyRepr
:: TCMTypeRepr t
=> Sing (x :: Hakaru)
-> t
-> Either Text (Some1 (Sing :: Hakaru -> *))
tyRepr :: Sing x -> t -> Either Text (Some1 Sing)
tyRepr Sing x
d = Either Text (Some1 Sing)
-> (Either Text (Some1 Sing) -> Either Text (Some1 Sing))
-> Maybe (Either Text (Some1 Sing))
-> Either Text (Some1 Sing)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Some1 Sing -> Either Text (Some1 Sing)
forall a b. b -> Either a b
Right (Some1 Sing -> Either Text (Some1 Sing))
-> Some1 Sing -> Either Text (Some1 Sing)
forall a b. (a -> b) -> a -> b
$ Sing x -> Some1 Sing
forall k (a :: k -> *) (i :: k). a i -> Some1 a
Some1 Sing x
d) Either Text (Some1 Sing) -> Either Text (Some1 Sing)
forall a. a -> a
id (Maybe (Either Text (Some1 Sing)) -> Either Text (Some1 Sing))
-> (t -> Maybe (Either Text (Some1 Sing)))
-> t
-> Either Text (Some1 Sing)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. t -> Maybe (Either Text (Some1 Sing))
forall x. TCMTypeRepr x => x -> Maybe (Either Text (Some1 Sing))
toTypeRepr
err :: Either Text (Sing x) -> Either Text (Sing y) -> TypeCheckMonad r
err = Metadata
-> Either Text (Sing x) -> Either Text (Sing y) -> TypeCheckMonad r
forall (a :: Hakaru) (b :: Hakaru) r.
Metadata
-> Either Text (Sing a) -> Either Text (Sing b) -> TypeCheckMonad r
typeMismatch Metadata
m
err :: Either Text (Sing (x :: Hakaru))
-> Either Text (Sing (y :: Hakaru))
-> TypeCheckMonad r
in case (Sing x -> t0 -> Either Text (Some1 Sing)
forall t (x :: Hakaru).
TCMTypeRepr t =>
Sing x -> t -> Either Text (Some1 Sing)
tyRepr Sing x
t0 t0
e0, Sing y -> t1 -> Either Text (Some1 Sing)
forall t (x :: Hakaru).
TCMTypeRepr t =>
Sing x -> t -> Either Text (Some1 Sing)
tyRepr Sing y
t1 t1
e1) of
(Left Text
a, Left Text
b) -> Either Text (Sing Any)
-> Either Text (Sing Any) -> TypeCheckMonad r
forall (x :: Hakaru) (y :: Hakaru) r.
Either Text (Sing x) -> Either Text (Sing y) -> TypeCheckMonad r
err (Text -> Either Text (Sing Any)
forall a b. a -> Either a b
Left Text
a) (Text -> Either Text (Sing Any)
forall a b. a -> Either a b
Left Text
b)
(Left Text
a, Right (Some1 Sing i
b)) -> Either Text (Sing Any) -> Either Text (Sing i) -> TypeCheckMonad r
forall (x :: Hakaru) (y :: Hakaru) r.
Either Text (Sing x) -> Either Text (Sing y) -> TypeCheckMonad r
err (Text -> Either Text (Sing Any)
forall a b. a -> Either a b
Left Text
a) (Sing i -> Either Text (Sing i)
forall a b. b -> Either a b
Right Sing i
b)
(Right (Some1 Sing i
a), Left Text
b) -> Either Text (Sing i) -> Either Text (Sing Any) -> TypeCheckMonad r
forall (x :: Hakaru) (y :: Hakaru) r.
Either Text (Sing x) -> Either Text (Sing y) -> TypeCheckMonad r
err (Sing i -> Either Text (Sing i)
forall a b. b -> Either a b
Right Sing i
a) (Text -> Either Text (Sing Any)
forall a b. a -> Either a b
Left Text
b)
(Right (Some1 Sing i
a), Right (Some1 Sing i
b)) -> Either Text (Sing i) -> Either Text (Sing i) -> TypeCheckMonad r
forall (x :: Hakaru) (y :: Hakaru) r.
Either Text (Sing x) -> Either Text (Sing y) -> TypeCheckMonad r
err (Sing i -> Either Text (Sing i)
forall a b. b -> Either a b
Right Sing i
a) (Sing i -> Either Text (Sing i)
forall a b. b -> Either a b
Right Sing i
b)