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