a1f8b40 · rowtype-yoga/purescript-native

git.iko.soy/rowtype-yoga/purescript-native

on golang help sign in

Replace type wildcards earlier (#2535)

a1f8b40Phil Freeman10 years ago

examples/failing/2534.pursnew file+8

compare with golang

unifiedsplit

@@ -0,0 +1,8 @@

1+-- @shouldFailWith InfiniteType

2+module Main where

4+foo :: Array Int -> Int

5+foo xs = go xs where

6+ go :: Array _ -> Int

7+ go [] = 0

8+ go xs = go [xs]

src/Language/PureScript/TypeChecker/Kinds.hs+1

@@ -229,6 +229,7 @@ infer' other = (, []) <$> go other

229 unifyKinds k k'

230 return k'

231 go TypeWildcard{} = freshKind

232+ go TUnknown{} = freshKind

232 go (TypeLevelString _) = return kindSymbol

233 go (TypeLevelString _) = return kindSymbol

233 go (TypeVar v) = do

234 go (TypeVar v) = do

234 Just moduleName <- checkCurrentModule <$> get

235 Just moduleName <- checkCurrentModule <$> get

src/Language/PureScript/TypeChecker/Types.hs+130−109

@@ -34,13 +34,14 @@ import Control.Monad.Supply.Class (MonadSupply)

34import Control.Monad.Writer.Class (MonadWriter(..))

36import Data.Bifunctor (bimap)

37−import Data.Either (lefts, rights)

37+import Data.Either (partitionEithers)

38import Data.Functor (($>))

39import Data.List (transpose, nub, (\\), partition, delete)

40import Data.Maybe (fromMaybe)

41import Data.Monoid ((<>))

42import qualified Data.Map as M

43import qualified Data.Set as S

44+import Data.Traversable (for)

45import Language.PureScript.AST

46import Language.PureScript.AST

46import Language.PureScript.Crash

47import Language.PureScript.Crash

@@ -62,7 +63,6 @@ import Language.PureScript.Types

62import Language.PureScript.Label (Label(..))

63import Language.PureScript.Label (Label(..))

63import Language.PureScript.PSString (PSString)

64import Language.PureScript.PSString (PSString)

65−

66data BindingGroupType

67 = RecursiveBindingGroup

68 | NonRecursiveBindingGroup

@@ -78,9 +78,9 @@ typesOf

78 -> m [(Ident, (Expr, Type))]

79typesOf bindingGroupType moduleName vals = withFreshSubstitution $ do

80 tys <- capturingSubstitution tidyUp $ do

81− (untyped, typed, dict, untypedDict) <- typeDictionaryForBindingGroup (Just moduleName) vals

81+ SplitBindingGroup untyped typed dict <- typeDictionaryForBindingGroup (Just moduleName) vals

82 ds1 <- parU typed $ \e -> withoutWarnings $ checkTypedBindingGroupElement moduleName e dict

83− ds2 <- forM untyped $ \e -> withoutWarnings $ typeForBindingGroupElement e dict untypedDict

83+ ds2 <- forM untyped $ \e -> withoutWarnings $ typeForBindingGroupElement e dict

84 return (map (False, ) ds1 ++ map (True, ) ds2)

86 inferred <- forM tys $ \(shouldGeneralize, ((ident, (val, ty)), _)) -> do

@@ -166,81 +166,101 @@ typesOf bindingGroupType moduleName vals = withFreshSubstitution $ do

166 isHoleError (ErrorMessage _ HoleInferredType{}) = True

167 isHoleError _ = False

168

169+-- | A binding group contains multiple value definitions, some of which are typed

170+-- and some which are not.

171+--

172+-- This structure breaks down a binding group into typed and untyped parts.

173+data SplitBindingGroup = SplitBindingGroup

174+ { _splitBindingGroupUntyped :: [(Ident, (Expr, Type))]

175+ -- ^ The untyped expressions

176+ , _splitBindingGroupTyped :: [(Ident, (Expr, Type, Bool))]

177+ -- ^ The typed expressions, along with their type annotations

169−type TypeData = M.Map (Qualified Ident) (Type, NameKind, NameVisibility)

178+ , _splitBindingGroupNames :: M.Map (Qualified Ident) (Type, NameKind, NameVisibility)

170−

179+ -- ^ A map containing all expressions and their assigned types (which might be

171−type UntypedData = [(Ident, Type)]

180+ -- fresh unification variables). These will be added to the 'Environment' after

172−

181+ -- the binding group is checked, so the value type of the 'Map' is chosen to be

182+ -- compatible with the type of 'bindNames'.

183+ }

184+

185+-- | This function breaks a binding group down into two sets of declarations:

186+-- those which contain type annotations, and those which don't.

187+-- This function also generates fresh unification variables for the types of

188+-- declarations without type annotations, returned in the 'UntypedData' structure.

173typeDictionaryForBindingGroup

189typeDictionaryForBindingGroup

174− :: (MonadState CheckState m)

190+ :: (MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m)

175 => Maybe ModuleName

191 => Maybe ModuleName

176 -> [(Ident, Expr)]

192 -> [(Ident, Expr)]

177− -> m ([(Ident, Expr)], [(Ident, (Expr, Type, Bool))], TypeData, UntypedData)

193+ -> m SplitBindingGroup

178typeDictionaryForBindingGroup moduleName vals = do

194typeDictionaryForBindingGroup moduleName vals = do

179− let

195+ -- Filter the typed and untyped declarations and make a map of names to typed declarations.

180− -- Map each declaration to a name/value pair, with an optional type, if the declaration is typed

196+ -- Replace type wildcards here so that the resulting dictionary of types contains the

181− es = map isTyped vals

197+ -- fully expanded types.

182− -- Filter the typed and untyped declarations

198+ let (untyped, typed) = partitionEithers (map splitTypeAnnotation vals)

183− untyped = lefts es

199+ (typedDict, typed') <- fmap unzip . for typed $ \(ident, (expr, ty, checkType)) -> do

184− typed = rights es

200+ ty' <- introduceSkolemScope <=< replaceAllTypeSynonyms <=< replaceTypeWildcards $ ty

185− -- Make a map of names to typed declarations

201+ return ((ident, ty'), (ident, (expr, ty', checkType)))

186− typedDict = map (\(ident, (_, ty, _)) -> (ident, ty)) typed

187−

188− -- Create fresh unification variables for the types of untyped declarations

202+ -- Create fresh unification variables for the types of untyped declarations

189− untypedNames <- replicateM (length untyped) freshType

203+ (untypedDict, untyped') <- fmap unzip . for untyped $ \(ident, expr) -> do

190−

204+ ty <- freshType

191− let

205+ return ((ident, ty), (ident, (expr, ty)))

192− -- Make a map of names to the unification variables of untyped declarations

193− untypedDict = zip (map fst untyped) untypedNames

194− -- Create the dictionary of all name/type pairs, which will be added to the environment during type checking

206+ -- Create the dictionary of all name/type pairs, which will be added to the

207+ -- environment during type checking

195− dict = M.fromList (map (\(ident, ty) -> (Qualified moduleName ident, (ty, Private, Undefined))) $ typedDict ++ untypedDict)

208+ let dict = M.fromList [ (Qualified moduleName ident, (ty, Private, Undefined))

196− return (untyped, typed, dict, untypedDict)

209+ | (ident, ty) <- typedDict <> untypedDict

197−

210+ ]

211+ return (SplitBindingGroup untyped' typed' dict)

212+ where

213+ -- | Check if a value contains a type annotation, and if so, separate it

214+ -- from the value itself.

215+ splitTypeAnnotation :: (Ident, Expr) -> Either (Ident, Expr) (Ident, (Expr, Type, Bool))

216+ splitTypeAnnotation (name, TypedValue checkType value ty) = Right (name, (value, ty, checkType))

217+ splitTypeAnnotation (name, PositionedValue pos c value) =

218+ bimap (second (PositionedValue pos c))

219+ (second (\(e, t, b) -> (PositionedValue pos c e, t, b)))

220+ (splitTypeAnnotation (name, value))

221+ splitTypeAnnotation (name, value) = Left (name, value)

222+

223+-- | Check the type annotation of a typed value in a binding group.

198checkTypedBindingGroupElement

224checkTypedBindingGroupElement

199 :: (MonadSupply m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m)

225 :: (MonadSupply m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m)

200 => ModuleName

226 => ModuleName

201 -> (Ident, (Expr, Type, Bool))

227 -> (Ident, (Expr, Type, Bool))

202− -> TypeData

228+ -- ^ The identifier we are trying to define, along with the expression and its type annotation

229+ -> M.Map (Qualified Ident) (Type, NameKind, NameVisibility)

230+ -- ^ Names brought into scope in this binding group

203 -> m (Ident, (Expr, Type))

231 -> m (Ident, (Expr, Type))

204−checkTypedBindingGroupElement mn (ident, (val', ty, checkType)) dict = do

232+checkTypedBindingGroupElement mn (ident, (val, ty, checkType)) dict = do

205− -- Replace type wildcards

206− ty' <- replaceTypeWildcards ty

207 -- Kind check

233 -- Kind check

208 (kind, args) <- kindOfWithScopedVars ty

234 (kind, args) <- kindOfWithScopedVars ty

209 checkTypeKind ty kind

235 checkTypeKind ty kind

210 -- Check the type with the new names in scope

236 -- Check the type with the new names in scope

211− ty'' <- introduceSkolemScope <=< replaceAllTypeSynonyms <=< replaceTypeWildcards $ ty'

212− val'' <- if checkType

237+ val' <- if checkType

213− then withScopedTypeVars mn args $ bindNames dict $ TypedValue True <$> check val' ty'' <*> pure ty''

238+ then withScopedTypeVars mn args $ bindNames dict $ TypedValue True <$> check val ty <*> pure ty

214− else return (TypedValue False val' ty'')

239+ else return (TypedValue False val ty)

215− return (ident, (val'', ty''))

240+ return (ident, (val', ty))

216

241

242+-- | Infer a type for a value in a binding group which lacks an annotation.

217typeForBindingGroupElement

243typeForBindingGroupElement

218 :: (MonadSupply m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m)

244 :: (MonadSupply m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m)

219− => (Ident, Expr)

245+ => (Ident, (Expr, Type))

220− -> TypeData

246+ -- ^ The identifier we are trying to define, along with the expression and its assigned type

221− -> UntypedData

247+ -- (at this point, this should be a unification variable)

248+ -> M.Map (Qualified Ident) (Type, NameKind, NameVisibility)

249+ -- ^ Names brought into scope in this binding group

222 -> m (Ident, (Expr, Type))

250 -> m (Ident, (Expr, Type))

223−typeForBindingGroupElement (ident, val) dict untypedDict = do

251+typeForBindingGroupElement (ident, (val, ty)) dict = do

224 -- Infer the type with the new names in scope

252 -- Infer the type with the new names in scope

225− TypedValue _ val' ty <- bindNames dict $ infer val

253+ TypedValue _ val' ty' <- bindNames dict $ infer val

226− unifyTypes ty $ fromMaybe (internalError "name not found in dictionary") (lookup ident untypedDict)

254+ -- Unify the type with the unification variable we chose for this definition

255+ unifyTypes ty ty'

227− return (ident, (TypedValue True val' ty, ty))

256+ return (ident, (TypedValue True val' ty', ty'))

228−

229−-- | Check if a value contains a type annotation

230−isTyped :: (Ident, Expr) -> Either (Ident, Expr) (Ident, (Expr, Type, Bool))

231−isTyped (name, TypedValue checkType value ty) = Right (name, (value, ty, checkType))

232−isTyped (name, PositionedValue pos c value) =

233− bimap (second (PositionedValue pos c))

234− (second (\(e, t, b) -> (PositionedValue pos c e, t, b)))

235− (isTyped (name, value))

236−isTyped (name, value) = Left (name, value)

237

257

238-- | Check the kind of a type, failing if it is not of kind *.

258-- | Check the kind of a type, failing if it is not of kind *.

239−checkTypeKind ::

259+checkTypeKind

240− (MonadError MultipleErrors m) =>

260+ :: MonadError MultipleErrors m

241− Type ->

261+ => Type

242− Kind ->

262+ -> Kind

243− m ()

263+ -> m ()

244checkTypeKind ty kind = guardWith (errorMessage (ExpectedType ty kind)) $ kind == kindType

264checkTypeKind ty kind = guardWith (errorMessage (ExpectedType ty kind)) $ kind == kindType

245

265

246-- | Remove any ForAlls and ConstrainedType constructors in a type by introducing new unknowns

266-- | Remove any ForAlls and ConstrainedType constructors in a type by introducing new unknowns

@@ -248,11 +268,11 @@ checkTypeKind ty kind = guardWith (errorMessage (ExpectedType ty kind)) $ kind =

248--

268--

249-- This is necessary during type checking to avoid unifying a polymorphic type with a

269-- This is necessary during type checking to avoid unifying a polymorphic type with a

250-- unification variable.

270-- unification variable.

251−instantiatePolyTypeWithUnknowns ::

271+instantiatePolyTypeWithUnknowns

252− (MonadState CheckState m, MonadError MultipleErrors m) =>

272+ :: (MonadState CheckState m, MonadError MultipleErrors m)

253− Expr ->

273+ => Expr

254− Type ->

274+ -> Type

255− m (Expr, Type)

275+ -> m (Expr, Type)

256instantiatePolyTypeWithUnknowns val (ForAll ident ty _) = do

276instantiatePolyTypeWithUnknowns val (ForAll ident ty _) = do

257 ty' <- replaceVarWithUnknown ident ty

277 ty' <- replaceVarWithUnknown ident ty

258 instantiatePolyTypeWithUnknowns val ty'

278 instantiatePolyTypeWithUnknowns val ty'

@@ -263,17 +283,17 @@ instantiatePolyTypeWithUnknowns val (ConstrainedType constraints ty) = do

263instantiatePolyTypeWithUnknowns val ty = return (val, ty)

283instantiatePolyTypeWithUnknowns val ty = return (val, ty)

264

284

265-- | Infer a type for a value, rethrowing any error to provide a more useful error message

285-- | Infer a type for a value, rethrowing any error to provide a more useful error message

266−infer ::

286+infer

267− (MonadSupply m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>

287+ :: (MonadSupply m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m)

268− Expr ->

288+ => Expr

269− m Expr

289+ -> m Expr

270infer val = withErrorMessageHint (ErrorInferringType val) $ infer' val

290infer val = withErrorMessageHint (ErrorInferringType val) $ infer' val

271

291

272-- | Infer a type for a value

292-- | Infer a type for a value

273−infer' ::

293+infer'

274− (MonadSupply m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>

294+ :: (MonadSupply m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m)

275− Expr ->

295+ => Expr

276− m Expr

296+ -> m Expr

277infer' v@(Literal (NumericLiteral (Left _))) = return $ TypedValue True v tyInt

297infer' v@(Literal (NumericLiteral (Left _))) = return $ TypedValue True v tyInt

278infer' v@(Literal (NumericLiteral (Right _))) = return $ TypedValue True v tyNumber

298infer' v@(Literal (NumericLiteral (Right _))) = return $ TypedValue True v tyNumber

279infer' v@(Literal (StringLiteral _)) = return $ TypedValue True v tyString

299infer' v@(Literal (StringLiteral _)) = return $ TypedValue True v tyString

@@ -370,13 +390,13 @@ infer' (PositionedValue pos c val) = warnAndRethrowWithPositionTC pos $ do

370 return $ TypedValue t (PositionedValue pos c v) ty

390 return $ TypedValue t (PositionedValue pos c v) ty

371infer' v = internalError $ "Invalid argument to infer: " ++ show v

391infer' v = internalError $ "Invalid argument to infer: " ++ show v

372

392

373−inferLetBinding ::

393+inferLetBinding

374− (MonadSupply m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>

394+ :: (MonadSupply m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m)

375− [Declaration] ->

395+ => [Declaration]

376− [Declaration] ->

396+ -> [Declaration]

377− Expr ->

397+ -> Expr

378− (Expr -> m Expr) ->

398+ -> (Expr -> m Expr)

379− m ([Declaration], Expr)

399+ -> m ([Declaration], Expr)

380inferLetBinding seen [] ret j = (,) seen <$> withBindingGroupVisible (j ret)

400inferLetBinding seen [] ret j = (,) seen <$> withBindingGroupVisible (j ret)

381inferLetBinding seen (ValueDeclaration ident nameKind [] (Right (tv@(TypedValue checkType val ty))) : rest) ret j = do

401inferLetBinding seen (ValueDeclaration ident nameKind [] (Right (tv@(TypedValue checkType val ty))) : rest) ret j = do

382 Just moduleName <- checkCurrentModule <$> get

402 Just moduleName <- checkCurrentModule <$> get

@@ -394,9 +414,9 @@ inferLetBinding seen (ValueDeclaration ident nameKind [] (Right val) : rest) ret

394 bindNames (M.singleton (Qualified Nothing ident) (valTy', nameKind, Defined)) $ inferLetBinding (seen ++ [ValueDeclaration ident nameKind [] (Right val')]) rest ret j

414 bindNames (M.singleton (Qualified Nothing ident) (valTy', nameKind, Defined)) $ inferLetBinding (seen ++ [ValueDeclaration ident nameKind [] (Right val')]) rest ret j

395inferLetBinding seen (BindingGroupDeclaration ds : rest) ret j = do

415inferLetBinding seen (BindingGroupDeclaration ds : rest) ret j = do

396 Just moduleName <- checkCurrentModule <$> get

416 Just moduleName <- checkCurrentModule <$> get

397− (untyped, typed, dict, untypedDict) <- typeDictionaryForBindingGroup Nothing (map (\(i, _, v) -> (i, v)) ds)

417+ SplitBindingGroup untyped typed dict <- typeDictionaryForBindingGroup Nothing (map (\(i, _, v) -> (i, v)) ds)

398 ds1' <- parU typed $ \e -> checkTypedBindingGroupElement moduleName e dict

418 ds1' <- parU typed $ \e -> checkTypedBindingGroupElement moduleName e dict

399− ds2' <- forM untyped $ \e -> typeForBindingGroupElement e dict untypedDict

419+ ds2' <- forM untyped $ \e -> typeForBindingGroupElement e dict

400 let ds' = [(ident, Private, val') | (ident, (val', _)) <- ds1' ++ ds2']

420 let ds' = [(ident, Private, val') | (ident, (val', _)) <- ds1' ++ ds2']

401 bindNames dict $ do

421 bindNames dict $ do

402 makeBindingGroupVisible

422 makeBindingGroupVisible

@@ -407,11 +427,12 @@ inferLetBinding seen (PositionedDeclaration pos com d : ds) ret j = warnAndRethr

407inferLetBinding _ _ _ _ = internalError "Invalid argument to inferLetBinding"

427inferLetBinding _ _ _ _ = internalError "Invalid argument to inferLetBinding"

408

428

409-- | Infer the types of variables brought into scope by a binder

429-- | Infer the types of variables brought into scope by a binder

410−inferBinder :: forall m.

430+inferBinder

431+ :: forall m

411− (MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>

432+ . (MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m)

412− Type ->

433+ => Type

413− Binder ->

434+ -> Binder

414− m (M.Map Ident Type)

435+ -> m (M.Map Ident Type)

415inferBinder _ NullBinder = return M.empty

436inferBinder _ NullBinder = return M.empty

416inferBinder val (LiteralBinder (StringLiteral _)) = unifyTypes val tyString >> return M.empty

437inferBinder val (LiteralBinder (StringLiteral _)) = unifyTypes val tyString >> return M.empty

417inferBinder val (LiteralBinder (CharLiteral _)) = unifyTypes val tyChar >> return M.empty

438inferBinder val (LiteralBinder (CharLiteral _)) = unifyTypes val tyChar >> return M.empty

@@ -486,11 +507,11 @@ binderRequiresMonotype (PositionedBinder _ _ b) = binderRequiresMonotype b

486binderRequiresMonotype _ = True

507binderRequiresMonotype _ = True

487

508

488-- | Instantiate polytypes only when necessitated by a binder.

509-- | Instantiate polytypes only when necessitated by a binder.

489−instantiateForBinders ::

510+instantiateForBinders

490− (MonadSupply m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>

511+ :: (MonadSupply m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m)

491− [Expr] ->

512+ => [Expr]

492− [CaseAlternative] ->

513+ -> [CaseAlternative]

493− m ([Expr], [Type])

514+ -> m ([Expr], [Type])

494instantiateForBinders vals cas = unzip <$> zipWithM (\val inst -> do

515instantiateForBinders vals cas = unzip <$> zipWithM (\val inst -> do

495 TypedValue _ val' ty <- infer val

516 TypedValue _ val' ty <- infer val

496 if inst

517 if inst

@@ -503,12 +524,12 @@ instantiateForBinders vals cas = unzip <$> zipWithM (\val inst -> do

503-- |

524-- |

504-- Check the types of the return values in a set of binders in a case statement

525-- Check the types of the return values in a set of binders in a case statement

505--

526--

506−checkBinders ::

527+checkBinders

507− (MonadSupply m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>

528+ :: (MonadSupply m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m)

508− [Type] ->

529+ => [Type]

509− Type ->

530+ -> Type

510− [CaseAlternative] ->

531+ -> [CaseAlternative]

511− m [CaseAlternative]

532+ -> m [CaseAlternative]

512checkBinders _ _ [] = return []

533checkBinders _ _ [] = return []

513checkBinders nvals ret (CaseAlternative binders result : bs) = do

534checkBinders nvals ret (CaseAlternative binders result : bs) = do

514 guardWith (errorMessage $ OverlappingArgNames Nothing) $

535 guardWith (errorMessage $ OverlappingArgNames Nothing) $

@@ -532,11 +553,11 @@ checkBinders nvals ret (CaseAlternative binders result : bs) = do

532-- |

553-- |

533-- Check the type of a value, rethrowing errors to provide a better error message

554-- Check the type of a value, rethrowing errors to provide a better error message

534--

555--

535−check ::

556+check

536− (MonadSupply m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>

557+ :: (MonadSupply m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m)

537− Expr ->

558+ => Expr

538− Type ->

559+ -> Type

539− m Expr

560+ -> m Expr

540check val ty = withErrorMessageHint (ErrorCheckingType val ty) $ check' val ty

561check val ty = withErrorMessageHint (ErrorCheckingType val ty) $ check' val ty

541

562

542-- |

563-- |

@@ -679,13 +700,13 @@ check' val ty = do

679--

700--

680-- The @lax@ parameter controls whether or not every record member has to be provided. For object updates, this is not the case.

701-- The @lax@ parameter controls whether or not every record member has to be provided. For object updates, this is not the case.

681--

702--

682−checkProperties ::

703+checkProperties

683− (MonadSupply m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>

704+ :: (MonadSupply m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m)

684− Expr ->

705+ => Expr

685− [(PSString, Expr)] ->

706+ -> [(PSString, Expr)]

686− Type ->

707+ -> Type

687− Bool ->

708+ -> Bool

688− m [(PSString, Expr)]

709+ -> m [(PSString, Expr)]

689checkProperties expr ps row lax = let (ts, r') = rowToList row in go ps ts r' where

710checkProperties expr ps row lax = let (ts, r') = rowToList row in go ps ts r' where

690 go [] [] REmpty = return []

711 go [] [] REmpty = return []

691 go [] [] u@(TUnknown _)

712 go [] [] u@(TUnknown _)