Mitigate exponential behaviour of inhabitance checker (#296)

This adds a simpler version of the inhabitance checker in pmcheck.
Unlike pmcheck's, this does not use any contextual information, which
means it can be memoized.

There are some cases where the exponential behaviour is still present.
For instance, consider the chain of sum types:

   type t1 'a = T1 of 'a
   type t2 'a 'b = T1L of (t1 'a) | T1R of (t1 'a)
   type t3 'a 'b = T3L of (t2 'a) | T3R of (t2 'a)
   (* ... *)

We cannot statically tell if tn is inhabited for any type variable. I
guess we could compile this to a predicate based on the type variables,
but that may be going a bit far :).

Fixes #294

Author: SquidDev

.ghci

@@ -1,8 +1,8 @@
 import qualified System.Environment as E
 :seti -XOverloadedStrings -XFlexibleContexts
 
-:def r! const (pure (unlines [ ":!tools/repl.sh reload", "::r", ":!tput bel" ]))
-:def reload! const (pure (unlines [ ":!tools/repl.sh reload", "::r", ":!tput bel" ]))
+:def! r! const (pure (unlines [ ":!tools/repl.sh reload", "::r", ":!tput bel" ]))
+:def! reload! const (pure (unlines [ ":!tools/repl.sh reload", "::r", ":!tput bel" ]))
 
 :def test \x -> pure $ ":!stack test --fast " ++ concat [ " --test-arguments '-p " ++ x ++ "'" | x /= "" ]
 :def test! const (pure ":!stack test --fast --test-arguments '-r'")

amuletml.cabal

@@ -321,6 +321,7 @@ library
                      , Types.Holes
                      , Types.Kinds
                      , Types.Unify
+                     , Types.Inhabited
                      , Types.Infer.Let
                      , Types.Infer.App
                      , Types.Unify.Base

bin/Prove.hs

@@ -204,11 +204,11 @@ env =
          & constructors %~ mappend cons
   where
     cons = Set.fromList [TgInternal "L", TgInternal "R", TgInternal "Not", TgInternal "T", TgInternal "Equiv"]
-    tys = Map.fromList [ (TgInternal "+", Set.fromList [TgInternal "L", TgInternal "R"])
-                       , (TgInternal "not", Set.fromList [TgInternal "Not"])
-                       , (TgInternal "ff", mempty)
-                       , (TgInternal "tt", Set.fromList [TgInternal "T"])
-                       , (TgInternal "<->", Set.fromList [TgInternal "Equiv"])
+    tys = Map.fromList [ (TgInternal "+", TypeDef (Set.fromList [TgInternal "L", TgInternal "R"]) Unknown)
+                       , (TgInternal "not", TypeDef (Set.fromList [TgInternal "Not"]) Unknown)
+                       , (TgInternal "ff", TypeDef mempty Uninhabited)
+                       , (TgInternal "tt", TypeDef (Set.fromList [TgInternal "T"]) Inhabited)
+                       , (TgInternal "<->", TypeDef (Set.fromList [TgInternal "Equiv"]) Unknown)
                        ]
 
     bindings = [ (TgInternal "+", TyType :-> TyType :-> TyType)

src/Syntax/Builtin.hs

@@ -197,7 +197,7 @@ data BuiltinPowule = BM
   { vars         :: [(Var Resolved, Type Typed)]
   , types        :: [(Var Resolved, Type Typed)]
   , modules      :: [(Var Resolved, BuiltinPowule)]
-  , constructors :: Map.Map (Var Resolved) (Set.Set (Var Typed))
+  , constructors :: Map.Map (Var Resolved) T.TypeDef
   , classes      :: [(Var Resolved, T.ClassInfo)]
   , families     :: [(Var Resolved, T.TySymInfo)]
   }
@@ -249,7 +249,8 @@ builtins =
             ]
 
   , constructors = Map.fromList
-      [ (tyListName, Set.fromList [cONSName, nILName] )
+      [ ( tyListName
+        , T.TypeDef (Set.fromList [cONSName, nILName]) T.Inhabited )
       ]
 
   , classes = [ (tyEqName, T.MagicInfo [] Nothing)
@@ -299,7 +300,10 @@ builtins =
                                                          , ( [1, 3], [2, 0], internal ) ]
                                                          Nothing )
                              ]
-                 , constructors = Map.fromList [(tyErrMsg_n, Set.fromList [tyeString_n, tyHCat_n, tyVCat_n, tyShowType_n])]
+                 , constructors = Map.fromList
+                    [ ( tyErrMsg_n
+                      , T.TypeDef (Set.fromList [tyeString_n, tyHCat_n, tyVCat_n, tyShowType_n]) T.Inhabited )
+                    ]
                  }
         ) ]
   , families = [ (tyTypeError_n, T.TyFamInfo { T._tsName = tyTypeError_n

src/Syntax/Types.hs

@@ -4,6 +4,7 @@
 module Syntax.Types
   ( Telescope, one, foldTele, foldTeleM, teleFromList, mapTele, traverseTele, teleToList
   , Scope(..), namesInScope, inScope, scopeToList, mapScope
+  , Inhabited(..), TypeDef(..), tdConstructors, tdInhabited
   , Env, freeInEnv, difference, envOf, scopeFromList, toMap
   , names, typeVars, constructors, types, letBound, classes
   , classDecs, tySyms, declaredHere
@@ -77,14 +78,26 @@ instance OrdPhrase p => Ixed (Scope p f) where
 instance OrdPhrase p => At (Scope p f) where
   at k f (Scope m) = Scope <$> at k f m
 
+data Inhabited
+  = Inhabited --- Type is unconditionally inhabited.
+  | Uninhabited --- Type is unconditionally uninhabited.
+  | Unknown --- Cannot be known.
+  deriving (Eq, Show, Ord)
+
+data TypeDef = TypeDef
+  { _tdConstructors :: Set.Set (Var Typed)
+  , _tdInhabited    :: Inhabited
+  }
+  deriving (Eq, Show, Ord)
+
 data Env
   = Env { _names        :: Scope Resolved (Type Typed)
         , _classes      :: ImplicitScope ClassInfo Typed
         , _typeVars     :: Set.Set (Var Typed)
         , _constructors :: Set.Set (Var Typed)
         , _letBound     :: Set.Set (Var Typed)
         , _declaredHere :: Set.Set (Var Typed) -- Only types
-        , _types        :: Map.Map (Var Typed) (Set.Set (Var Typed))
+        , _types        :: Map.Map (Var Typed) TypeDef
         , _classDecs    :: Map.Map (Var Typed) ClassInfo
         , _tySyms       :: TySyms
         }
@@ -166,6 +179,7 @@ instance Show DerivingStrat where
 instance Ord DerivingStrat where
   _ `compare` _ = GT
 
+makeLenses ''TypeDef
 makeLenses ''Env
 makeLenses ''ClassInfo
 makeLenses ''TySymInfo

src/Syntax/Verify.hs

@@ -109,7 +109,7 @@ verifyProgram = traverse_ verifyStmt where
           TgName n _ -> n <> T.singleton '.'
           TgInternal v -> v <> T.singleton '.'
         ext s = s { env = env s & names %~ mapScope id (unqualifyWrt prefix)
-                                & types %~ fmap (Set.mapMonotonic (unqualifyVarWrt prefix)) }
+                                & types %~ fmap (tdConstructors %~ Set.mapMonotonic (unqualifyVarWrt prefix)) }
 
     local ext $ verifyModule m
 

src/Syntax/Verify/Pattern.hs

@@ -420,7 +420,7 @@ constructors env kty vty = do
   where
     -- | Get the constructors for a given type
     ctors :: Type Typed -> Set.Set (Var Typed)
-    ctors (TyCon v _) = fromMaybe (error $ "Cannot find constructors for " ++ show v) (env ^. (types . at v))
+    ctors (TyCon v _) = maybe (error $ "Cannot find constructors for " ++ show v) _tdConstructors (env ^. (types . at v))
     ctors (TyApp f _) = ctors f
     ctors t = error $ "Cannot get type name from " ++ show (pretty t)
 
@@ -496,10 +496,15 @@ inhabited env (AbsState st cs i)
   ctorCheck :: (MonadPlus m, MonadNamey m, MonadState CoverState m)
             => Set.Set (Var Typed) -> Type Typed -> m ()
   ctorCheck c t
-    | Just v <- concreteTy c t = do
-        let c' = Set.insert v c
-        (_, arg) <- constructors env t t
-        maybe inhb (go c') arg
+    | Just v <- concreteTy c t =
+        case maybe Unknown _tdInhabited (env ^. (types . at v)) of
+          Uninhabited -> mzero
+          Inhabited -> inhb
+          Unknown ->
+            do
+            let c' = Set.insert v c
+            (_, arg) <- constructors env t t
+            maybe inhb (go c') arg
     | otherwise = inhb
 
 -- | Make a unification constraint

src/Types/Holes.hs

@@ -121,7 +121,7 @@ fill t | t == tyUnit = fake [t] $ pure . Literal LiUnit . head
 -- Sum types: we need to try each constructor.
 fill ty@(TyApps (TyCon ty_v ()) _) = once (knownImplication ty) <|> do
   -- Search all constructors for the type..
-  con <- explore =<< view (psEnv . types . at ty_v . non mempty . to Set.toList)
+  con <- explore =<< views (psEnv . types . at ty_v) (maybe mempty (Set.toList . _tdConstructors))
 #ifdef TRACE_TC
   traceM (displayS (keyword "try" <+> pretty con))
 #endif
@@ -178,7 +178,7 @@ fill _ = fail ""
 makeFunction :: MonadPs m => Type Typed -> Type Typed -> m (Expr Typed)
 makeFunction domain@(TyApps (TyCon t ()) _) body_t = fake [domain] $ \[ann] -> do
   span <- view psAnn
-  cons <- view (psEnv . types . at t . non undefined . to Set.toList)
+  cons <- view (psEnv . types . at t . non undefined . tdConstructors . to Set.toList)
 
   arms <- for cons $ \con -> do
     (ty, _) <- skolGadt con =<<
@@ -205,7 +205,7 @@ isSum (TyOperator l o r) = isSum (TyApps o [l, r])
 isSum (TyApps (TyCon t ()) _) = do
   x <- view (psEnv . types . at t)
   pure $ case x of
-    Just t -> Set.size t /= 1
+    Just t -> Set.size (t ^. tdConstructors) /= 1
     Nothing -> False
 isSum _ = pure False
 
@@ -289,7 +289,7 @@ assume ty@(TyExactRows xs) k = go [] xs k where
   go pats [] k = fake [ty] $ \[record] -> k (PRecord (reverse pats) record)
 
 assume ty@(TyApps (TyCon c ()) xs) k = fake [ty] $ \[pat] -> do
-  cs <- view (psEnv . types . at c . non mempty . to Set.toList)
+  cs <- views (psEnv . types . at c) (maybe mempty (Set.toList . _tdConstructors))
   case cs of
     [con] -> do
       ~(ty, _) <- skolGadt con =<<

src/Types/Infer.hs

@@ -42,6 +42,7 @@ import Types.Infer.Builtin
 import Types.Infer.Class
 import Types.Infer.App
 import Types.Infer.Let
+import Types.Inhabited
 import Types.Kinds
 import Types.Unify
 
@@ -536,8 +537,9 @@ inferProg (decl@(TypeDecl am n tvs cs ann):prg) = do
           (for cs (\con -> retcons (addBlame (BecauseOf con)) (inferCon vars retTy con)))
 
         let ts' = Set.fromList (map fst ts)
+        inhabited <- asks (\env -> inhabited env n cs')
         local ( (names %~ focus (teleFromList ts))
-                . (types %~ Map.insert n ts')
+                . (types %~ Map.insert n (TypeDef ts' inhabited))
                 . (constructors %~ Set.union ts') ) $
           cont (Just cs')
 
@@ -640,7 +642,8 @@ inferMod (ModStruct bod a) = do
            let diff = env `difference` extEnv
                env' = (declaredHere .~ mempty)
                     . (names .~ mapScope (append prefix) (qualifyWrt prefix) (diff ^. names))
-                    . (types .~ (Set.mapMonotonic (append prefix) <$> Map.mapKeysMonotonic (append prefix) (diff ^. types)))
+                    . (types .~ ((tdConstructors %~ Set.mapMonotonic (append prefix))
+                                 <$> Map.mapKeysMonotonic (append prefix) (diff ^. types)))
                     $  env
            in extEnv <> env')
 
@@ -774,7 +777,7 @@ unqualify (ModRef v _) =
          TgName v _ -> v <> T.singleton '.'
          TgInternal v -> v <> T.singleton '.'
   in (names %~ mapScope id (unqualifyWrt prefix))
-   . (types %~ fmap (Set.mapMonotonic (unqualifyVarWrt prefix)))
+   . (types %~ fmap (tdConstructors %~ Set.mapMonotonic (unqualifyVarWrt prefix)))
 
 unqualify _ = id
 

src/Types/Inhabited.hs

@@ -0,0 +1,72 @@
+{-# LANGUAGE FlexibleContexts, TypeFamilies, ScopedTypeVariables #-}
+
+{-| A simplified version of pmcheck's inhabited type checker. This determines
+if a type is:
+ - Trivially inhabitable (i.e. has an inhabitable constructor),
+ - Uninhabitable (all constructors are uninhabitable), or
+ - Unknown (relies on additional information, such as constraints or type variables)
+-}
+module Types.Inhabited (inhabited) where
+
+import Control.Lens
+
+import Syntax.Var
+import Syntax.Type
+import Syntax.Types
+import Syntax.Toplevel
+
+inhabited :: forall p. Var p ~ VarResolved
+          => Env -> Var p -> [Constructor p] -> Inhabited
+inhabited env tyName = goCtors where
+  goCtors :: [Constructor p] -> Inhabited
+  goCtors [] = Uninhabited
+  goCtors (UnitCon{}:_) = Inhabited
+  goCtors (ArgCon _ _ t _:cs) = orInhabited (goType t) (goCtors cs)
+  goCtors (GadtCon{}:cs) =
+    -- :( I cannot think of a way to do this sensibly, so we let the verifier
+    -- check this for us.
+    orInhabited Unknown (goCtors cs)
+
+  goTypes :: [Type p] -> Inhabited
+  goTypes [] = Inhabited
+  goTypes (t:ts) =
+      case goType t of
+          Inhabited -> goTypes ts
+          x -> x
+
+  goType :: Type p -> Inhabited
+  -- We can't know if a type variable is inhabited or not!
+  goType TyVar{} = Unknown
+
+  goType (TyApp t _) = goType t
+  goType (TyCon v _)
+    | v == tyName = Unknown
+    | otherwise = case env ^. types . at v of
+        Nothing -> Inhabited -- Abstract types are considered inhabited.
+        Just t -> t ^. tdInhabited
+
+  -- We don't really have the concept of uninhabited types, so we assume
+  -- type names are.
+  goType TyPromotedCon{} = Inhabited
+  -- For now, we'll just assume all Pi types are inhabited. Thankfully,
+  -- they all are.
+  goType TyPi{} = Inhabited
+  -- All the boring types: just determine if the children are inhabited
+  goType (TyRows f fs) = goTypes (f:map snd fs)
+  goType (TyExactRows fs) = goTypes (snd <$> fs)
+  goType (TyTuple l r) = goTypes [l, r]
+  goType (TyOperator l v r) = goType (TyApp (TyApp v l) r)
+  goType (TyWildcard t) = maybe Unknown goType t
+  goType (TyParens t) = goType t
+
+  goType TySkol{} = Inhabited
+  goType (TyWithConstraints _ t) = goType t
+  goType TyType = Inhabited
+  goType TyLit{} = Inhabited
+  goType TyTupleL{} = Inhabited
+
+orInhabited :: Inhabited -> Inhabited -> Inhabited
+orInhabited Inhabited _ = Inhabited
+orInhabited Uninhabited x = x
+orInhabited Unknown Inhabited = Inhabited
+orInhabited Unknown _ = Unknown

tests/verify/pmcheck/exponential_inhabit.ml

@@ -0,0 +1,61 @@
+(**
+  Checks exponential behaviour of the inhabitation checker.
+
+  Note: putting a type variable in all of these will still cause issues. We just
+  rely on the fact that you'll have concrete boundaries somewhere. I'm not smart
+  enough to do this correctly.
+*)
+
+type t0 = T0 of int
+type t1 = T1 of t0 * t0
+type t2 = T2 of t1 * t1
+type t3 = T3 of t2 * t2
+type t4 = T4 of t3 * t3
+type t5 = T5 of t4 * t4
+type t6 = T6 of t5 * t5
+type t7 = T7 of t6 * t6
+type t8 = T8 of t7 * t7
+type t9 = T9 of t8 * t8
+type t10 = T10 of t9 * t9
+type t11 = T11 of t10 * t10
+type t12 = T12 of t11 * t11
+type t13 = T13 of t12 * t12
+type t14 = T14 of t13 * t13
+type t15 = T15 of t14 * t14
+type t16 = T16 of t15 * t15
+type t17 = T17 of t16 * t16
+type t18 = T18 of t17 * t17
+type t19 = T19 of t18 * t18
+type t20 = T20 of t19 * t19
+type t21 = T21 of t20 * t20
+type t22 = T22 of t21 * t21
+type t23 = T23 of t22 * t22
+type t24 = T24 of t23 * t23
+type t25 = T25 of t24 * t24
+type t26 = T26 of t25 * t25
+type t27 = T27 of t26 * t26
+type t28 = T28 of t27 * t27
+type t29 = T29 of t28 * t28
+type t30 = T30 of t29 * t29
+type t31 = T31 of t30 * t30
+type t32 = T32 of t31 * t31
+type t33 = T33 of t32 * t32
+type t34 = T34 of t33 * t33
+type t35 = T35 of t34 * t34
+type t36 = T36 of t35 * t35
+type t37 = T37 of t36 * t36
+type t38 = T38 of t37 * t37
+type t39 = T39 of t38 * t38
+type t40 = T40 of t39 * t39
+type t41 = T41 of t40 * t40
+type t42 = T42 of t41 * t41
+type t43 = T43 of t42 * t42
+type t44 = T44 of t43 * t43
+type t45 = T45 of t44 * t44
+type t46 = T46 of t45 * t45
+type t47 = T47 of t46 * t46
+type t48 = T48 of t47 * t47
+type t49 = T49 of t48 * t48
+type t50 = T50 of t49 * t49
+
+let f (T50 _) = ()