Make singleSubst perform checks and return Either type.

The old `singleSubst` has been renamed to `uncheckedSingleSubst`.

Fixes #723.

src/Cryptol/TypeCheck/Default.hs

@@ -9,7 +9,7 @@ import Control.Monad(guard)
 import Cryptol.TypeCheck.Type
 import Cryptol.TypeCheck.SimpType(tMax,tWidth)
 import Cryptol.TypeCheck.Error(Warning(..))
-import Cryptol.TypeCheck.Subst(Subst,apSubst,listSubst,substBinds,singleSubst)
+import Cryptol.TypeCheck.Subst(Subst,apSubst,listSubst,substBinds,uncheckedSingleSubst)
 import Cryptol.TypeCheck.InferTypes(Goal,goal,Goals(..),goalsFromList)
 import Cryptol.TypeCheck.Solver.SMT(Solver,tryGetModel,shrinkModel)
 import Cryptol.Utils.Panic(panic)
@@ -152,7 +152,7 @@ improveByDefaultingWithPure as ps =
           let ty  = case ts of
                       [] -> tNum (0::Int)
                       _  -> foldr1 tMax ts
-              su1 = singleSubst x ty
+              su1 = uncheckedSingleSubst x ty
           in ( (x,ty) : [ (y,apSubst su1 t) | (y,t) <- yes ]
              , no         -- We know that `x` does not appear here
              , otherFree  -- We know that `x` did not appear here either

src/Cryptol/TypeCheck/Solver/Improve.hs

@@ -51,7 +51,7 @@ improveLit impSkol prop =
      (_,b) <- aSeq t
      a     <- aTVar b
      unless impSkol $ guard (isFreeTV a)
-     let su = singleSubst a tBit
+     let su = uncheckedSingleSubst a tBit
      return (su, [])
 
 
@@ -66,13 +66,15 @@ improveEq impSkol fins prop =
   where
   rewrite this other =
     do x <- aTVar this
-       guard (considerVar x && x `Set.notMember` fvs other)
-       return (singleSubst x other, [])
+       guard (considerVar x)
+       case singleSubst x other of
+         Left _ -> mzero
+         Right su -> return (su, [])
     <|>
     do (v,s) <- isSum this
-       guard (v `Set.notMember` fvs other)
-       return (singleSubst v (Mk.tSub other s), [ other >== s ])
-
+       case singleSubst v (Mk.tSub other s) of
+         Left _ -> mzero
+         Right su -> return (su, [ other >== s ])
 
   isSum t = do (v,s) <- matches t (anAdd, aTVar, __)
                valid v s

src/Cryptol/TypeCheck/Subst.hs

@@ -14,8 +14,10 @@
 module Cryptol.TypeCheck.Subst
   ( Subst
   , emptySubst
+  , SubstError(..)
   , singleSubst
   , singleTParamSubst
+  , uncheckedSingleSubst
   , (@@)
   , defaultingSubst
   , listSubst
@@ -75,20 +77,38 @@ emptySubst =
     , suDefaulting = False
     }
 
-singleSubst :: TVar -> Type -> Subst
-singleSubst v@(TVFree i _ _tps _) t =
+-- | Reasons to reject a single-variable substitution.
+data SubstError
+  = SubstRecursive
+  -- ^ 'TVar' maps to a type containing the same variable.
+  | SubstEscaped [TParam]
+  -- ^ 'TVar' maps to a type containing one or more out-of-scope bound variables.
+
+singleSubst :: TVar -> Type -> Either SubstError Subst
+singleSubst x t
+  | x `Set.member` fvs t   = Left SubstRecursive
+  | not (Set.null escaped) = Left (SubstEscaped (Set.toList escaped))
+  | otherwise              = Right (uncheckedSingleSubst x t)
+  where
+    escaped =
+      case x of
+        TVBound _ -> Set.empty
+        TVFree _ _ scope _ -> freeParams t `Set.difference` scope
+
+uncheckedSingleSubst :: TVar -> Type -> Subst
+uncheckedSingleSubst v@(TVFree i _ _tps _) t =
   S { suFreeMap = IntMap.singleton i (v, t)
     , suBoundMap = IntMap.empty
     , suDefaulting = False
     }
-singleSubst v@(TVBound tp) t =
+uncheckedSingleSubst v@(TVBound tp) t =
   S { suFreeMap = IntMap.empty
     , suBoundMap = IntMap.singleton (tpUnique tp) (v, t)
     , suDefaulting = False
     }
 
 singleTParamSubst :: TParam -> Type -> Subst
-singleTParamSubst tp t = singleSubst (TVBound tp) t
+singleTParamSubst tp t = uncheckedSingleSubst (TVBound tp) t
 
 (@@) :: Subst -> Subst -> Subst
 s2 @@ s1
@@ -338,4 +358,3 @@ instance TVars DeclDef where
 
 instance TVars Module where
   apSubst su m = m { mDecls = apSubst su (mDecls m) }
-

src/Cryptol/TypeCheck/Unify.hs

@@ -111,14 +111,17 @@ bindVar v@(TVBound {}) t
   where k = kindOf v
 
 bindVar x@(TVFree _ _ xscope _) (TVar y@(TVFree _ _ yscope _))
-  | xscope `Set.isProperSubsetOf` yscope = return (singleSubst y (TVar x), [])
+  | xscope `Set.isProperSubsetOf` yscope =
+    return (uncheckedSingleSubst y (TVar x), [])
 
-bindVar x@(TVFree _ k inScope _d) t
+bindVar x@(TVFree _ k _scope _d) t
   | not (k == kindOf t)     = uniError $ UniKindMismatch k (kindOf t)
-  | recTy && k == KType     = uniError $ UniRecursive x t
-  | not (Set.null escaped)  = uniError $ UniNonPolyDepends x $ Set.toList escaped
-  | recTy                   = return (emptySubst, [TVar x =#= t])
-  | otherwise               = return (singleSubst x t, [])
-    where
-    escaped = freeParams t `Set.difference` inScope
-    recTy   = x `Set.member` fvs t
+  | otherwise               =
+    case singleSubst x t of
+      Left SubstRecursive
+        | k == KType -> uniError $ UniRecursive x t
+        | otherwise  -> return (emptySubst, [TVar x =#= t])
+      Left (SubstEscaped tps) ->
+        uniError $ UniNonPolyDepends x tps
+      Right su ->
+        return (su, [])