constrained-generators: Make type errors clearer using the csongor

MaximilianAlgehed · MaximilianAlgehed · commit 524d715e131d · 2025-04-29T06:29:00.000+02:00
trick
diff --git a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Instances/Ledger.hs b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Instances/Ledger.hs
@@ -393,6 +393,7 @@ instance
       err = error $ "toCompact @" ++ show (typeOf x) ++ " " ++ show x
 instance
   ( Compactible a
+  , GenericallyInstantiated (CompactForm a)
   , Typeable (TypeSpec (SimpleRep a))
   , Show (TypeSpec (SimpleRep a))
   , HasSpec a
@@ -873,7 +874,13 @@ instance Typeable a => HasSimpleRep (THKD tag Identity a) where
   type SimpleRep (THKD tag Identity a) = a
   fromSimpleRep = THKD
   toSimpleRep (THKD a) = a
-instance (IsNormalType a, Typeable tag, HasSpec a) => HasSpec (THKD tag Identity a)
+instance
+  ( IsNormalType a
+  , Typeable tag
+  , HasSpec a
+  , GenericallyInstantiated (THKD tag Identity a)
+  ) =>
+  HasSpec (THKD tag Identity a)
 
 instance HasSimpleRep GovActionPurpose
 instance HasSpec GovActionPurpose
diff --git a/libs/constrained-generators/constrained-generators.cabal b/libs/constrained-generators/constrained-generators.cabal
@@ -45,6 +45,7 @@ library
     Constrained.SumList
     Constrained.Syntax
     Constrained.TheKnot
+    Constrained.TypeErrors
 
   hs-source-dirs: src
   default-language: Haskell2010
diff --git a/libs/constrained-generators/src/Constrained/API.hs b/libs/constrained-generators/src/Constrained/API.hs
@@ -5,6 +5,7 @@
 {-# LANGUAGE ViewPatterns #-}
 
 module Constrained.API (
+  GenericallyInstantiated,
   Logic (..),
   Semantics (..),
   Syntax (..),
@@ -144,6 +145,7 @@ where
 
 import Constrained.Base (
   Fun (..),
+  GenericallyInstantiated,
   HasSpec (..),
   Logic (..),
   Pred (..),
diff --git a/libs/constrained-generators/src/Constrained/Base.hs b/libs/constrained-generators/src/Constrained/Base.hs
@@ -24,7 +24,7 @@
 {-# LANGUAGE UndecidableSuperClasses #-}
 {-# LANGUAGE ViewPatterns #-}
 -- Show Evidence
-{-# OPTIONS_GHC -Wno-orphans #-}
+{-# OPTIONS_GHC -Wno-orphans -Wno-unticked-promoted-constructors #-}
 
 -- | This module contains the most basic parts the implementation. Essentially
 --   everything to define Specification, HasSpec, HasSimpleRep, Term, Pred, and the Syntax,
@@ -71,6 +71,7 @@ import Constrained.List (
   pattern ListCtx,
   pattern NilCtx,
  )
+import Constrained.TypeErrors
 
 import Control.Monad.Writer (
   Writer,
@@ -383,7 +384,66 @@ typeSpec ts = TypeSpec ts mempty
 -- Don't be afraid of all the methods. Most have default implementations.
 -- =================================================================
 
-class (Typeable a, Eq a, Show a, Show (TypeSpec a), Typeable (TypeSpec a)) => HasSpec a where
+type GenericallyInstantiated a =
+  ( AssertComputes
+      (SimpleRep a)
+      ( Text "Trying to use a generic instantiation of "
+          :<>: ShowType a
+          :<>: Text ", likely in a HasSpec instance."
+          :$$: Text
+                "However, the type has no definition of SimpleRep, likely because of a missing instance of HasSimpleRep."
+      )
+  , HasSimpleRep a
+  , HasSpec (SimpleRep a)
+  , TypeSpec a ~ TypeSpec (SimpleRep a)
+  )
+
+type TypeSpecEqShow a =
+  ( AssertComputes
+      (TypeSpec a)
+      ( Text "Can't compute "
+          :<>: ShowType (TypeSpec a)
+          :$$: Text "Either because of a missing definition of TypeSpec or a missing instance of HasSimpleRep."
+      )
+  , Show (TypeSpec a)
+  , Typeable (TypeSpec a)
+  )
+
+{- NOTE: type errors in constrained-generators
+    It's easy to make a mistake like this:
+      data Bad = Bad | Worse deriving (Eq, Show)
+      instance HasSpec Bad
+    Missing that this requires an instance of HasSimpleRep for Bad to work.
+    The two `AssertComputes` uses above are here to give you better error messages when you make this mistake,
+    e.g. giving you something like this:
+      src/Constrained/Examples/Basic.hs:327:10: error: [GHC-64725]
+          • Can't compute TypeSpec (SimpleRep Bad)
+            Either because of a missing definition of TypeSpec or a missing instance of HasSimpleRep.
+          • In the instance declaration for ‘HasSpec Bad’
+          |
+      327 | instance HasSpec Bad
+          |          ^^^^^^^^^^^
+
+      src/Constrained/Examples/Basic.hs:327:10: error: [GHC-64725]
+          • Trying to use a generic instantiation of Bad, likely in a HasSpec instance.
+            However, the type has no definition of SimpleRep, likely because of a missing instance of HasSimpleRep.
+          • In the expression: Constrained.Base.$dmemptySpec @(Bad)
+            In an equation for ‘emptySpec’:
+                emptySpec = Constrained.Base.$dmemptySpec @(Bad)
+            In the instance declaration for ‘HasSpec Bad’
+          |
+      327 | instance HasSpec Bad
+          |          ^^^^^^^^^^^
+-}
+
+class
+  ( Typeable a
+  , Eq a
+  , Show a
+  , TypeSpecEqShow a
+  ) =>
+  HasSpec a
+  where
   -- | The `TypeSpec a` is the type-specific `Specification a`.
   type TypeSpec a
 
@@ -489,63 +549,45 @@ class (Typeable a, Eq a, Show a, Show (TypeSpec a), Typeable (TypeSpec a)) => Ha
      a` using `fromSimpleRepSpec`.
    -}
 
-  default emptySpec ::
-    (HasSpec (SimpleRep a), TypeSpec a ~ TypeSpec (SimpleRep a)) => TypeSpec a
+  default emptySpec :: GenericallyInstantiated a => TypeSpec a
   emptySpec = emptySpec @(SimpleRep a)
 
   default combineSpec ::
-    ( HasSimpleRep a
-    , HasSpec (SimpleRep a)
-    , TypeSpec a ~ TypeSpec (SimpleRep a)
-    ) =>
+    GenericallyInstantiated a =>
     TypeSpec a ->
     TypeSpec a ->
     Specification a
   combineSpec s s' = fromSimpleRepSpec $ combineSpec @(SimpleRep a) s s'
 
   default genFromTypeSpec ::
-    ( HasSimpleRep a
-    , HasSpec (SimpleRep a)
-    , TypeSpec a ~ TypeSpec (SimpleRep a)
-    ) =>
-    (HasCallStack, MonadGenError m) =>
+    (GenericallyInstantiated a, HasCallStack, MonadGenError m) =>
     TypeSpec a ->
     GenT m a
   genFromTypeSpec s = fromSimpleRep <$> genFromTypeSpec s
 
   default conformsTo ::
-    ( HasSimpleRep a
-    , HasSpec (SimpleRep a)
-    , TypeSpec a ~ TypeSpec (SimpleRep a)
-    ) =>
-    HasCallStack =>
+    (GenericallyInstantiated a, HasCallStack) =>
     a ->
     TypeSpec a ->
     Bool
   a `conformsTo` s = conformsTo (toSimpleRep a) s
 
   default toPreds ::
-    ( HasSpec (SimpleRep a)
-    , TypeSpec a ~ TypeSpec (SimpleRep a)
-    , HasSimpleRep a
-    ) =>
+    GenericallyInstantiated a =>
     Term a ->
     TypeSpec a ->
     Pred
   toPreds v s = toPreds (toGeneric_ v) s
 
   default shrinkWithTypeSpec ::
-    ( HasSpec (SimpleRep a)
-    , TypeSpec a ~ TypeSpec (SimpleRep a)
-    , HasSimpleRep a
-    ) =>
+    GenericallyInstantiated a =>
     TypeSpec a ->
     a ->
     [a]
   shrinkWithTypeSpec spec a = map fromSimpleRep $ shrinkWithTypeSpec spec (toSimpleRep a)
 
   default cardinalTypeSpec ::
-    (HasSpec (SimpleRep a), TypeSpec a ~ TypeSpec (SimpleRep a)) =>
+    GenericallyInstantiated a =>
     TypeSpec a ->
     Specification Integer
   cardinalTypeSpec = cardinalTypeSpec @(SimpleRep a)
diff --git a/libs/constrained-generators/src/Constrained/NumSpec.hs b/libs/constrained-generators/src/Constrained/NumSpec.hs
@@ -17,6 +17,7 @@
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE UndecidableSuperClasses #-}
 {-# LANGUAGE ViewPatterns #-}
 -- Random Natural, Arbitrary Natural, Uniform Natural
 {-# OPTIONS_GHC -Wno-orphans #-}
diff --git a/libs/constrained-generators/src/Constrained/Properties.hs b/libs/constrained-generators/src/Constrained/Properties.hs
@@ -162,9 +162,9 @@ prop_conformEmpty ::
 prop_conformEmpty a = QC.property $ conformsTo a (emptySpec @a)
 
 prop_univSound :: TestableFn -> QC.Property
-prop_univSound (TestableFn fn) =
+prop_univSound (TestableFn (fn :: t as b)) =
   QC.label (show fn) $
-    QC.forAllShrinkBlind QC.arbitrary QC.shrink $ \tc@(TestableCtx ctx) ->
+    QC.forAllShrinkBlind @QC.Property (QC.arbitrary @(TestableCtx as)) QC.shrink $ \tc@(TestableCtx ctx) ->
       QC.forAllShrinkBlind QC.arbitrary QC.shrink $ \spec ->
         QC.counterexample ("\nfn ctx = " ++ showCtxWith fn tc) $
           QC.counterexample (show $ "\nspec =" <+> pretty spec) $
@@ -221,7 +221,7 @@ showCtxWith fn (TestableCtx ctx) = show tm
     tm :: Term b
     tm =
       uncurryList (appTerm fn) $
-        fillListCtx (mapListCtxC @HasSpec (lit @_ . unValue) ctx) (\HOLE -> V $ Var 0 "v")
+        fillListCtx (mapListCtxC @HasSpec @_ @Value @Term (lit @_ . unValue) ctx) (\HOLE -> V $ Var 0 "v")
 
 data TestableFn where
   TestableFn ::
diff --git a/libs/constrained-generators/src/Constrained/Spec/SumProd.hs b/libs/constrained-generators/src/Constrained/Spec/SumProd.hs
@@ -18,6 +18,7 @@
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE UndecidableSuperClasses #-}
 {-# LANGUAGE ViewPatterns #-}
 {-# OPTIONS_GHC -Wno-orphans #-}
 {-# OPTIONS_GHC -Wno-redundant-constraints #-}
diff --git a/libs/constrained-generators/src/Constrained/SumList.hs b/libs/constrained-generators/src/Constrained/SumList.hs
@@ -9,6 +9,7 @@
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableSuperClasses #-}
 {-# LANGUAGE ViewPatterns #-}
 
 -- | Operations for generating random elements of Num like types, that sum to a particular total.
diff --git a/libs/constrained-generators/src/Constrained/Syntax.hs b/libs/constrained-generators/src/Constrained/Syntax.hs
@@ -601,6 +601,7 @@ runCaseOn s ((x :-> ps) :> bs@(_ :> _)) f = case s of
 letSubexpressionElimination :: HasSpec Bool => Pred -> Pred
 letSubexpressionElimination = go []
   where
+    adjustSub :: HasSpec a => Var a -> Subst -> Subst
     adjustSub x sub =
       [ x' := t
       | x' := t <- sub
@@ -663,6 +664,7 @@ letFloating = fold . go []
   where
     goBlock ctx ps = goBlock' (freeVarNames ctx <> freeVarNames ps) ctx ps
 
+    goBlock' :: Set Int -> [Pred] -> [Pred] -> [Pred]
     goBlock' _ ctx [] = ctx
     goBlock' fvs ctx (Let t (x :-> p) : ps) =
       -- We can do `goBlock'` here because we've already done let floating
diff --git a/libs/constrained-generators/src/Constrained/TheKnot.hs b/libs/constrained-generators/src/Constrained/TheKnot.hs
@@ -27,6 +27,7 @@
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE UndecidableSuperClasses #-}
 {-# LANGUAGE ViewPatterns #-}
 {-# OPTIONS_GHC -Wno-orphans -Wno-name-shadowing #-}
 
@@ -779,6 +780,7 @@ aggressiveInlining pred
 
     underBinder fvs x p = fvs `without` [Name x] <> singleton (Name x) (countOf (Name x) p)
 
+    underBinderSub :: HasSpec a => Subst -> Var a -> Subst
     underBinderSub sub x =
       [ x' := t
       | x' := t <- sub
@@ -1294,6 +1296,7 @@ shrinkFromPreds p
 shrinkEnvFromPlan :: Env -> SolverPlan -> [Env]
 shrinkEnvFromPlan initialEnv SolverPlan {..} = go mempty solverPlan
   where
+    go :: Env -> [SolverStage] -> [Env]
     go _ [] = [] -- In this case we decided to keep every variable the same so nothing to return
     go env ((substStage env -> SolverStage {..}) : plan) = do
       Just a <- [lookupEnv initialEnv stageVar]
@@ -1308,6 +1311,7 @@ shrinkEnvFromPlan initialEnv SolverPlan {..} = go mempty solverPlan
         ++ go (extendEnv stageVar a env) plan
 
     -- Fix the rest of the plan given an environment `env` for the plan so far
+    fixupPlan :: Env -> [SolverStage] -> Maybe Env
     fixupPlan env [] = pure env
     fixupPlan env ((substStage env -> SolverStage {..}) : plan) =
       case lookupEnv initialEnv stageVar >>= fixupWithSpec stageSpec of
@@ -1534,6 +1538,7 @@ backPropagation :: SolverPlan -> SolverPlan
 -- backPropagation (SolverPlan _plan _graph) =
 backPropagation (SolverPlan initplan graph) = SolverPlan (go [] (reverse initplan)) graph
   where
+    go :: [SolverStage] -> [SolverStage] -> [SolverStage]
     go acc [] = acc
     go acc (s@(SolverStage (x :: Var a) ps spec) : plan) = go (s : acc) plan'
       where
diff --git a/libs/constrained-generators/src/Constrained/TypeErrors.hs b/libs/constrained-generators/src/Constrained/TypeErrors.hs
@@ -0,0 +1,55 @@
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# OPTIONS_GHC -Wno-unticked-promoted-constructors #-}
+
+module Constrained.TypeErrors (
+  AssertComputes,
+  module X,
+) where
+
+import Data.Kind
+#if MIN_VERSION_base(4,17,0)
+import GHC.TypeError as X
+#else
+import GHC.TypeLits as X
+#endif
+
+-- NOTE: this module implementes this very neat little trick for observing when type
+-- families are stuck https://blog.csongor.co.uk/report-stuck-families/ which allows
+-- us to report much better type errors when our generics tricks fail.
+--
+-- The idea of this type family is that if `ty` evaluates to a type (other than Dummy which
+-- we haven't exported) then `Computes ty (TE err)` will evaluate to `()` without
+-- getting stuck and without expanding `TE` to `TypeError err`.
+--
+-- If, on the other hand, GHC gets stuck evaluating `ty` it will (hopefully) try to normalize
+-- everything and (hopefully) end up with `Computes (TypeError err) ty` which in turn will cause
+-- it to throw `err` as a type error.
+--
+-- Now, the important thing here is that you can't do `Computes _ _ = ()` because that doesn't
+-- force the evaluation of `ty` and consequently doesn't end up with GHC wanting to report
+-- that `Computes tyThatDoesntCompute (TE err)` fails and consequently normalizing `TE err`
+-- and finally arriving at `TypeError err`.
+type family Computes (ty :: Type) (err :: Constraint) :: Constraint where
+  Computes Dummy _ =
+    TypeError
+      (Text "This shouldn't be reachable because " :<>: ShowType Dummy :<>: Text " shouldn't be exported!")
+  Computes _ _ = ()
+
+-- This is intentionally hidden in here to avoid any funny business
+data Dummy
+
+-- NOTE: this indirection is necessary only for older versions of GHC where this is
+-- "the right" amount of strictness - apparently it's not necessary on newer versions of GHC!
+-- The alternative would be to just do `AssertComputes ty em = Computes ty (TypeError em)` below
+-- and that works fine on e.g. ghc 9.12 (and other recent versions) but fails on 8.10.7 because
+-- GHC is "too eager" to throw the type error.
+type family TE em where
+  TE em = TypeError em
+
+type AssertComputes ty em = Computes ty (TE em)
diff --git a/libs/constrained-generators/test/Constrained/Test.hs b/libs/constrained-generators/test/Constrained/Test.hs
