{-# LANGUAGE Safe #-}
{-# LANGUAGE PatternGuards, ViewPatterns #-}
{-# LANGUAGE DeriveFunctor, DeriveGeneric, DeriveAnyClass #-}
{-# LANGUAGE BlockArguments, OverloadedStrings #-}
module Cryptol.TypeCheck.Unify where
import Control.DeepSeq(NFData)
import GHC.Generics(Generic)
import Cryptol.TypeCheck.AST
import Cryptol.TypeCheck.Subst
import Cryptol.Utils.RecordMap
import Cryptol.Utils.Ident(Ident)
import Cryptol.ModuleSystem.Name(nameIdent)
import Cryptol.TypeCheck.PP
import Control.Monad.Writer (Writer, writer, runWriter)
import qualified Data.Set as Set
import Prelude ()
import Prelude.Compat
type MGU = (Subst,[Prop])
type Result a = Writer [(Path,UnificationError)] a
runResult :: Result a -> (a, [(Path,UnificationError)])
runResult :: forall a. Result a -> (a, [(Path, UnificationError)])
runResult = Writer [(Path, UnificationError)] a
-> (a, [(Path, UnificationError)])
forall w a. Writer w a -> (a, w)
runWriter
data UnificationError
= UniTypeMismatch Type Type
| UniKindMismatch Kind Kind
| UniTypeLenMismatch Int Int
| UniRecursive TVar Type
| UniNonPolyDepends TVar [TParam]
| UniNonPoly TVar Type
uniError :: Path -> UnificationError -> Result MGU
uniError :: Path -> UnificationError -> Result MGU
uniError Path
p UnificationError
e = (MGU, [(Path, UnificationError)]) -> Result MGU
forall a.
(a, [(Path, UnificationError)])
-> WriterT [(Path, UnificationError)] Identity a
forall w (m :: * -> *) a. MonadWriter w m => (a, w) -> m a
writer (MGU
emptyMGU, [(Path
p,UnificationError
e)])
newtype Path = Path [PathElement]
deriving (Int -> Path -> ShowS
[Path] -> ShowS
Path -> String
(Int -> Path -> ShowS)
-> (Path -> String) -> ([Path] -> ShowS) -> Show Path
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Path -> ShowS
showsPrec :: Int -> Path -> ShowS
$cshow :: Path -> String
show :: Path -> String
$cshowList :: [Path] -> ShowS
showList :: [Path] -> ShowS
Show,(forall x. Path -> Rep Path x)
-> (forall x. Rep Path x -> Path) -> Generic Path
forall x. Rep Path x -> Path
forall x. Path -> Rep Path x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Path -> Rep Path x
from :: forall x. Path -> Rep Path x
$cto :: forall x. Rep Path x -> Path
to :: forall x. Rep Path x -> Path
Generic,Path -> ()
(Path -> ()) -> NFData Path
forall a. (a -> ()) -> NFData a
$crnf :: Path -> ()
rnf :: Path -> ()
NFData)
data PathElement =
TConArg TC Int
| TNominalArg NominalType Int
| TRecArg Ident
deriving (Int -> PathElement -> ShowS
[PathElement] -> ShowS
PathElement -> String
(Int -> PathElement -> ShowS)
-> (PathElement -> String)
-> ([PathElement] -> ShowS)
-> Show PathElement
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> PathElement -> ShowS
showsPrec :: Int -> PathElement -> ShowS
$cshow :: PathElement -> String
show :: PathElement -> String
$cshowList :: [PathElement] -> ShowS
showList :: [PathElement] -> ShowS
Show,(forall x. PathElement -> Rep PathElement x)
-> (forall x. Rep PathElement x -> PathElement)
-> Generic PathElement
forall x. Rep PathElement x -> PathElement
forall x. PathElement -> Rep PathElement x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. PathElement -> Rep PathElement x
from :: forall x. PathElement -> Rep PathElement x
$cto :: forall x. Rep PathElement x -> PathElement
to :: forall x. Rep PathElement x -> PathElement
Generic,PathElement -> ()
(PathElement -> ()) -> NFData PathElement
forall a. (a -> ()) -> NFData a
$crnf :: PathElement -> ()
rnf :: PathElement -> ()
NFData)
rootPath :: Path
rootPath :: Path
rootPath = [PathElement] -> Path
Path []
isRootPath :: Path -> Bool
isRootPath :: Path -> Bool
isRootPath (Path [PathElement]
xs) = [PathElement] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [PathElement]
xs
extPath :: Path -> PathElement -> Path
extPath :: Path -> PathElement -> Path
extPath (Path [PathElement]
xs) PathElement
x = [PathElement] -> Path
Path (PathElement
x PathElement -> [PathElement] -> [PathElement]
forall a. a -> [a] -> [a]
: [PathElement]
xs)
emptyMGU :: MGU
emptyMGU :: MGU
emptyMGU = (Subst
emptySubst, [])
doMGU :: Type -> Type -> Result MGU
doMGU :: Type -> Type -> Result MGU
doMGU Type
t1 Type
t2 = Path -> Type -> Type -> Result MGU
mgu Path
rootPath Type
t1 Type
t2
mgu :: Path -> Type -> Type -> Result MGU
mgu :: Path -> Type -> Type -> Result MGU
mgu Path
_ (TUser Name
c1 [Type]
ts1 Type
_) (TUser Name
c2 [Type]
ts2 Type
_)
| Name
c1 Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
c2 Bool -> Bool -> Bool
&& [Type]
ts1 [Type] -> [Type] -> Bool
forall a. Eq a => a -> a -> Bool
== [Type]
ts2 = MGU -> Result MGU
forall a. a -> WriterT [(Path, UnificationError)] Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return MGU
emptyMGU
mgu Path
p (TVar TVar
x) Type
t = Path -> TVar -> Type -> Result MGU
bindVar Path
p TVar
x Type
t
mgu Path
p Type
t (TVar TVar
x) = Path -> TVar -> Type -> Result MGU
bindVar Path
p TVar
x Type
t
mgu Path
p (TUser Name
_ [Type]
_ Type
t1) Type
t2 = Path -> Type -> Type -> Result MGU
mgu Path
p Type
t1 Type
t2
mgu Path
p Type
t1 (TUser Name
_ [Type]
_ Type
t2) = Path -> Type -> Type -> Result MGU
mgu Path
p Type
t1 Type
t2
mgu Path
p (TCon (TC TC
tc1) [Type]
ts1) (TCon (TC TC
tc2) [Type]
ts2)
| TC
tc1 TC -> TC -> Bool
forall a. Eq a => a -> a -> Bool
== TC
tc2 =
let paths :: [Path]
paths = [ Path -> PathElement -> Path
extPath Path
p (TC -> Int -> PathElement
TConArg TC
tc1 Int
i) | Int
i <- [ Int
0 .. ] ]
in Path -> [Path] -> [Type] -> [Type] -> Result MGU
mguMany Path
p [Path]
paths [Type]
ts1 [Type]
ts2
mgu Path
_ (TCon (TF TFun
f1) [Type]
ts1) (TCon (TF TFun
f2) [Type]
ts2)
| TFun
f1 TFun -> TFun -> Bool
forall a. Eq a => a -> a -> Bool
== TFun
f2 Bool -> Bool -> Bool
&& [Type]
ts1 [Type] -> [Type] -> Bool
forall a. Eq a => a -> a -> Bool
== [Type]
ts2 = MGU -> Result MGU
forall a. a -> WriterT [(Path, UnificationError)] Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return MGU
emptyMGU
mgu Path
_ Type
t1 Type
t2
| TCon (TF TFun
_) [Type]
_ <- Type
t1, Bool
isNum, Kind
k1 Kind -> Kind -> Bool
forall a. Eq a => a -> a -> Bool
== Kind
k2 = MGU -> Result MGU
forall a. a -> WriterT [(Path, UnificationError)] Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Subst
emptySubst, [Type
t1 Type -> Type -> Type
=#= Type
t2])
| TCon (TF TFun
_) [Type]
_ <- Type
t2, Bool
isNum, Kind
k1 Kind -> Kind -> Bool
forall a. Eq a => a -> a -> Bool
== Kind
k2 = MGU -> Result MGU
forall a. a -> WriterT [(Path, UnificationError)] Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Subst
emptySubst, [Type
t1 Type -> Type -> Type
=#= Type
t2])
where
k1 :: Kind
k1 = Type -> Kind
forall t. HasKind t => t -> Kind
kindOf Type
t1
k2 :: Kind
k2 = Type -> Kind
forall t. HasKind t => t -> Kind
kindOf Type
t2
isNum :: Bool
isNum = Kind
k1 Kind -> Kind -> Bool
forall a. Eq a => a -> a -> Bool
== Kind
KNum
mgu Path
p (TRec RecordMap Ident Type
fs1) (TRec RecordMap Ident Type
fs2)
| RecordMap Ident Type -> Set Ident
forall a b. Ord a => RecordMap a b -> Set a
fieldSet RecordMap Ident Type
fs1 Set Ident -> Set Ident -> Bool
forall a. Eq a => a -> a -> Bool
== RecordMap Ident Type -> Set Ident
forall a b. Ord a => RecordMap a b -> Set a
fieldSet RecordMap Ident Type
fs2 =
let paths :: [Path]
paths = [ Path -> PathElement -> Path
extPath Path
p (Ident -> PathElement
TRecArg Ident
i) | (Ident
i,Type
_) <- RecordMap Ident Type -> [(Ident, Type)]
forall a b. RecordMap a b -> [(a, b)]
canonicalFields RecordMap Ident Type
fs1 ]
in Path -> [Path] -> [Type] -> [Type] -> Result MGU
mguMany Path
p [Path]
paths (RecordMap Ident Type -> [Type]
forall a b. RecordMap a b -> [b]
recordElements RecordMap Ident Type
fs1) (RecordMap Ident Type -> [Type]
forall a b. RecordMap a b -> [b]
recordElements RecordMap Ident Type
fs2)
mgu Path
p (TNominal NominalType
ntx [Type]
xs) (TNominal NominalType
nty [Type]
ys)
| NominalType
ntx NominalType -> NominalType -> Bool
forall a. Eq a => a -> a -> Bool
== NominalType
nty =
let paths :: [Path]
paths = [ Path -> PathElement -> Path
extPath Path
p (NominalType -> Int -> PathElement
TNominalArg NominalType
ntx Int
i) | Int
i <- [ Int
0 .. ] ]
in Path -> [Path] -> [Type] -> [Type] -> Result MGU
mguMany Path
p [Path]
paths [Type]
xs [Type]
ys
mgu Path
p Type
t1 Type
t2
| Bool -> Bool
not (Kind
k1 Kind -> Kind -> Bool
forall a. Eq a => a -> a -> Bool
== Kind
k2) = Path -> UnificationError -> Result MGU
uniError Path
p (UnificationError -> Result MGU) -> UnificationError -> Result MGU
forall a b. (a -> b) -> a -> b
$ Kind -> Kind -> UnificationError
UniKindMismatch Kind
k1 Kind
k2
| Bool
otherwise = Path -> UnificationError -> Result MGU
uniError Path
p (UnificationError -> Result MGU) -> UnificationError -> Result MGU
forall a b. (a -> b) -> a -> b
$ Type -> Type -> UnificationError
UniTypeMismatch Type
t1 Type
t2
where
k1 :: Kind
k1 = Type -> Kind
forall t. HasKind t => t -> Kind
kindOf Type
t1
k2 :: Kind
k2 = Type -> Kind
forall t. HasKind t => t -> Kind
kindOf Type
t2
mguMany :: Path -> [Path] -> [Type] -> [Type] -> Result MGU
mguMany :: Path -> [Path] -> [Type] -> [Type] -> Result MGU
mguMany Path
_ [Path]
_ [] [] = MGU -> Result MGU
forall a. a -> WriterT [(Path, UnificationError)] Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return MGU
emptyMGU
mguMany Path
p (Path
p1:[Path]
ps) (Type
t1 : [Type]
ts1) (Type
t2 : [Type]
ts2) =
do (Subst
su1,[Type]
ps1) <- Path -> Type -> Type -> Result MGU
mgu Path
p1 Type
t1 Type
t2
(Subst
su2,[Type]
ps2) <- Path -> [Path] -> [Type] -> [Type] -> Result MGU
mguMany Path
p [Path]
ps (Subst -> [Type] -> [Type]
forall t. TVars t => Subst -> t -> t
apSubst Subst
su1 [Type]
ts1) (Subst -> [Type] -> [Type]
forall t. TVars t => Subst -> t -> t
apSubst Subst
su1 [Type]
ts2)
MGU -> Result MGU
forall a. a -> WriterT [(Path, UnificationError)] Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Subst
su2 Subst -> Subst -> Subst
@@ Subst
su1, [Type]
ps1 [Type] -> [Type] -> [Type]
forall a. [a] -> [a] -> [a]
++ [Type]
ps2)
mguMany Path
p [Path]
_ [Type]
t1 [Type]
t2 = Path -> UnificationError -> Result MGU
uniError Path
p (UnificationError -> Result MGU) -> UnificationError -> Result MGU
forall a b. (a -> b) -> a -> b
$ Int -> Int -> UnificationError
UniTypeLenMismatch ([Type] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
t1) ([Type] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
t2)
bindVar :: Path -> TVar -> Type -> Result MGU
bindVar :: Path -> TVar -> Type -> Result MGU
bindVar Path
_ TVar
x (Type -> Type
tNoUser -> TVar TVar
y)
| TVar
x TVar -> TVar -> Bool
forall a. Eq a => a -> a -> Bool
== TVar
y = MGU -> Result MGU
forall a. a -> WriterT [(Path, UnificationError)] Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return MGU
emptyMGU
bindVar Path
p v :: TVar
v@(TVBound {})
(Type -> Type
tNoUser -> TVar v1 :: TVar
v1@(TVFree {})) = Path -> TVar -> Type -> Result MGU
bindVar Path
p TVar
v1 (TVar -> Type
TVar TVar
v)
bindVar Path
p v :: TVar
v@(TVBound {}) Type
t
| Kind
k Kind -> Kind -> Bool
forall a. Eq a => a -> a -> Bool
== Type -> Kind
forall t. HasKind t => t -> Kind
kindOf Type
t = if Kind
k Kind -> Kind -> Bool
forall a. Eq a => a -> a -> Bool
== Kind
KNum
then MGU -> Result MGU
forall a. a -> WriterT [(Path, UnificationError)] Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Subst
emptySubst, [TVar -> Type
TVar TVar
v Type -> Type -> Type
=#= Type
t])
else Path -> UnificationError -> Result MGU
uniError Path
p (UnificationError -> Result MGU) -> UnificationError -> Result MGU
forall a b. (a -> b) -> a -> b
$ TVar -> Type -> UnificationError
UniNonPoly TVar
v Type
t
| Bool
otherwise = Path -> UnificationError -> Result MGU
uniError Path
p (UnificationError -> Result MGU) -> UnificationError -> Result MGU
forall a b. (a -> b) -> a -> b
$ Kind -> Kind -> UnificationError
UniKindMismatch Kind
k (Type -> Kind
forall t. HasKind t => t -> Kind
kindOf Type
t)
where k :: Kind
k = TVar -> Kind
forall t. HasKind t => t -> Kind
kindOf TVar
v
bindVar Path
_ x :: TVar
x@(TVFree Int
_ Kind
xk Set TParam
xscope TVarInfo
_) (Type -> Type
tNoUser -> TVar y :: TVar
y@(TVFree Int
_ Kind
yk Set TParam
yscope TVarInfo
_))
| Set TParam
xscope Set TParam -> Set TParam -> Bool
forall a. Ord a => Set a -> Set a -> Bool
`Set.isProperSubsetOf` Set TParam
yscope, Kind
xk Kind -> Kind -> Bool
forall a. Eq a => a -> a -> Bool
== Kind
yk =
MGU -> Result MGU
forall a. a -> WriterT [(Path, UnificationError)] Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (TVar -> Type -> Subst
uncheckedSingleSubst TVar
y (TVar -> Type
TVar TVar
x), [])
bindVar Path
p TVar
x Type
t =
case TVar -> Type -> Either SubstError Subst
singleSubst TVar
x Type
t of
Left SubstError
SubstRecursive
| TVar -> Kind
forall t. HasKind t => t -> Kind
kindOf TVar
x Kind -> Kind -> Bool
forall a. Eq a => a -> a -> Bool
== Kind
KType -> Path -> UnificationError -> Result MGU
uniError Path
p (UnificationError -> Result MGU) -> UnificationError -> Result MGU
forall a b. (a -> b) -> a -> b
$ TVar -> Type -> UnificationError
UniRecursive TVar
x Type
t
| Bool
otherwise -> MGU -> Result MGU
forall a. a -> WriterT [(Path, UnificationError)] Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Subst
emptySubst, [TVar -> Type
TVar TVar
x Type -> Type -> Type
=#= Type
t])
Left (SubstEscaped [TParam]
tps) ->
Path -> UnificationError -> Result MGU
uniError Path
p (UnificationError -> Result MGU) -> UnificationError -> Result MGU
forall a b. (a -> b) -> a -> b
$ TVar -> [TParam] -> UnificationError
UniNonPolyDepends TVar
x [TParam]
tps
Left (SubstKindMismatch Kind
k1 Kind
k2) ->
Path -> UnificationError -> Result MGU
uniError Path
p (UnificationError -> Result MGU) -> UnificationError -> Result MGU
forall a b. (a -> b) -> a -> b
$ Kind -> Kind -> UnificationError
UniKindMismatch Kind
k1 Kind
k2
Right Subst
su ->
MGU -> Result MGU
forall a. a -> WriterT [(Path, UnificationError)] Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Subst
su, [])
ppPathEl :: PathElement -> Int -> (Int -> Doc) -> Doc
ppPathEl :: PathElement -> Int -> (Int -> Doc) -> Doc
ppPathEl PathElement
el Int
prec Int -> Doc
k =
case PathElement
el of
TRecArg Ident
l -> Doc -> Doc
braces (Ident -> Doc
forall a. PP a => a -> Doc
pp Ident
l Doc -> Doc -> Doc
<+> Doc
":" Doc -> Doc -> Doc
<+> Int -> Doc
k Int
0 Doc -> Doc -> Doc
<.> Doc
comma Doc -> Doc -> Doc
<+> Doc
"…")
TConArg TC
tc Int
n ->
case TC
tc of
TC
TCSeq -> Bool -> Doc -> Doc
optParens (Int
prec Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
4)
if Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 then Doc -> Doc
brackets (Int -> Doc
k Int
0) Doc -> Doc -> Doc
<+> Doc
"_"
else Doc -> Doc
brackets Doc
"_" Doc -> Doc -> Doc
<+> (Int -> Doc
k Int
4)
TC
TCFun -> Bool -> Doc -> Doc
optParens (Int
prec Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
1)
if Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 then Int -> Doc
k Int
2 Doc -> Doc -> Doc
<+> Doc
"->" Doc -> Doc -> Doc
<+> Doc
"_"
else Doc
"_" Doc -> Doc -> Doc
<+> Doc
"->" Doc -> Doc -> Doc
<+> Int -> Doc
k Int
1
TCTuple Int
i -> Doc -> Doc
parens ([Doc] -> Doc
commaSep ([Doc]
before [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ [Int -> Doc
k Int
0] [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ [Doc]
after))
where before :: [Doc]
before = Int -> Doc -> [Doc]
forall a. Int -> a -> [a]
replicate Int
n Doc
"_"
after :: [Doc]
after = Int -> Doc -> [Doc]
forall a. Int -> a -> [a]
replicate (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) Doc
"_"
TC
_ -> Int -> Doc -> Int -> Doc
justPrefix (Kind -> Int
forall {a}. Num a => Kind -> a
kindArity (TC -> Kind
forall t. HasKind t => t -> Kind
kindOf TC
tc)) (TC -> Doc
forall a. PP a => a -> Doc
pp TC
tc) Int
n
TNominalArg NominalType
nt Int
n ->
Int -> Doc -> Int -> Doc
justPrefix ([TParam] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (NominalType -> [TParam]
ntParams NominalType
nt)) (Ident -> Doc
forall a. PP a => a -> Doc
pp (Name -> Ident
nameIdent (NominalType -> Name
ntName NominalType
nt))) Int
n
where
justPrefix :: Int -> Doc -> Int -> Doc
justPrefix Int
arity Doc
fun Int
n =
Bool -> Doc -> Doc
optParens (Int
prec Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
3) (Doc
fun Doc -> Doc -> Doc
<+> [Doc] -> Doc
hsep ([Doc]
before [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ [Int -> Doc
k Int
5] [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ [Doc]
after))
where before :: [Doc]
before = Int -> Doc -> [Doc]
forall a. Int -> a -> [a]
replicate Int
n Doc
"_"
after :: [Doc]
after = Int -> Doc -> [Doc]
forall a. Int -> a -> [a]
replicate (Int
arity Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) Doc
"_"
kindArity :: Kind -> a
kindArity Kind
ki =
case Kind
ki of
Kind
_ :-> Kind
k1 -> a
1 a -> a -> a
forall a. Num a => a -> a -> a
+ Kind -> a
kindArity Kind
k1
Kind
_ -> a
0
instance PP Path where
ppPrec :: Int -> Path -> Doc
ppPrec Int
prec0 (Path [PathElement]
ps0) = [PathElement] -> Int -> Doc
go ([PathElement] -> [PathElement]
forall a. [a] -> [a]
reverse [PathElement]
ps0) Int
prec0
where
go :: [PathElement] -> Int -> Doc
go [PathElement]
ps Int
prec =
case [PathElement]
ps of
[] -> Doc
"ERROR"
PathElement
p : [PathElement]
more -> PathElement -> Int -> (Int -> Doc) -> Doc
ppPathEl PathElement
p Int
prec ([PathElement] -> Int -> Doc
go [PathElement]
more)