1-- |
2-- Module      :  Cryptol.TypeCheck.Unify
3-- Copyright   :  (c) 2013-2016 Galois, Inc.
4-- License     :  BSD3
5-- Maintainer  :  cryptol@galois.com
6-- Stability   :  provisional
7-- Portability :  portable
8
9{-# LANGUAGE Safe #-}
10{-# LANGUAGE PatternGuards, ViewPatterns #-}
11{-# LANGUAGE DeriveFunctor #-}
12module Cryptol.TypeCheck.Unify where
13
14import Cryptol.TypeCheck.AST
15import Cryptol.TypeCheck.Subst
16import Cryptol.Utils.RecordMap
17
18import Control.Monad.Writer (Writer, writer, runWriter)
19import qualified Data.Set as Set
20
21import Prelude ()
22import Prelude.Compat
23
24-- | The most general unifier is a substitution and a set of constraints
25-- on bound variables.
26type MGU = (Subst,[Prop])
27
28type Result a = Writer [UnificationError] a
29
30runResult :: Result a -> (a, [UnificationError])
31runResult = runWriter
32
33data UnificationError
34  = UniTypeMismatch Type Type
35  | UniKindMismatch Kind Kind
36  | UniTypeLenMismatch Int Int
37  | UniRecursive TVar Type
38  | UniNonPolyDepends TVar [TParam]
39  | UniNonPoly TVar Type
40
41uniError :: UnificationError -> Result MGU
42uniError e = writer (emptyMGU, [e])
43
44
45emptyMGU :: MGU
46emptyMGU = (emptySubst, [])
47
48mgu :: Type -> Type -> Result MGU
49
50mgu (TUser c1 ts1 _) (TUser c2 ts2 _)
51  | c1 == c2 && ts1 == ts2  = return emptyMGU
52
53mgu (TVar x) t        = bindVar x t
54mgu t (TVar x)        = bindVar x t
55
56mgu (TUser _ _ t1) t2 = mgu t1 t2
57mgu t1 (TUser _ _ t2) = mgu t1 t2
58
59mgu (TCon (TC tc1) ts1) (TCon (TC tc2) ts2)
60  | tc1 == tc2 = mguMany ts1 ts2
61
62mgu (TCon (TF f1) ts1) (TCon (TF f2) ts2)
63  | f1 == f2 && ts1 == ts2  = return emptyMGU
64
65mgu t1 t2
66  | TCon (TF _) _ <- t1, isNum, k1 == k2 = return (emptySubst, [t1 =#= t2])
67  | TCon (TF _) _ <- t2, isNum, k1 == k2 = return (emptySubst, [t1 =#= t2])
68  where
69  k1 = kindOf t1
70  k2 = kindOf t2
71
72  isNum = k1 == KNum
73
74mgu (TRec fs1) (TRec fs2)
75  | fieldSet fs1 == fieldSet fs2 = mguMany (recordElements fs1) (recordElements fs2)
76
77mgu (TNewtype ntx xs) (TNewtype nty ys)
78  | ntx == nty = mguMany xs ys
79
80mgu t1 t2
81  | not (k1 == k2)  = uniError $ UniKindMismatch k1 k2
82  | otherwise       = uniError $ UniTypeMismatch t1 t2
83  where
84  k1 = kindOf t1
85  k2 = kindOf t2
86
87
88mguMany :: [Type] -> [Type] -> Result MGU
89mguMany [] [] = return emptyMGU
90mguMany (t1 : ts1) (t2 : ts2) =
91  do (su1,ps1) <- mgu t1 t2
92     (su2,ps2) <- mguMany (apSubst su1 ts1) (apSubst su1 ts2)
93     return (su2 @@ su1, ps1 ++ ps2)
94mguMany t1 t2 = uniError $ UniTypeLenMismatch (length t1) (length t2)
95
96
97bindVar :: TVar -> Type -> Result MGU
98
99bindVar x (tNoUser -> TVar y)
100  | x == y                      = return emptyMGU
101
102bindVar v@(TVBound {}) (tNoUser -> TVar v1@(TVFree {})) = bindVar v1 (TVar v)
103
104bindVar v@(TVBound {}) t
105  | k == kindOf t = if k == KNum
106                       then return (emptySubst, [TVar v =#= t])
107                       else uniError $ UniNonPoly v t
108  | otherwise     = uniError $ UniKindMismatch k (kindOf t)
109  where k = kindOf v
110
111bindVar x@(TVFree _ xk xscope _) (tNoUser -> TVar y@(TVFree _ yk yscope _))
112  | xscope `Set.isProperSubsetOf` yscope, xk == yk =
113    return (uncheckedSingleSubst y (TVar x), [])
114    -- In this case, we can add the reverse binding y ~> x to the
115    -- substitution, but the instantiation x ~> y would be forbidden
116    -- because it would allow y to escape from its scope.
117
118bindVar x t =
119  case singleSubst x t of
120    Left SubstRecursive
121      | kindOf x == KType -> uniError $ UniRecursive x t
122      | otherwise -> return (emptySubst, [TVar x =#= t])
123    Left (SubstEscaped tps) ->
124      uniError $ UniNonPolyDepends x tps
125    Left (SubstKindMismatch k1 k2) ->
126      uniError $ UniKindMismatch k1 k2
127    Right su ->
128      return (su, [])
129