Working around a GHC bug

plutus-core/src/Language/PlutusCore/Constant/Meaning.hs

@@ -160,7 +160,7 @@ with 'ToBinds' results in the following list of bindings:
 
 Higher-kinded type variables are fully supported.
 
-The implementation of the 'KnownMonotype' and 'KnownPolytype' classes are structured in an
+The implementations of the 'KnownMonotype' and 'KnownPolytype' classes are structured in an
 inference-friendly manner:
 
 1. we compute @args@ using a type family ('GetArgs') in order to dispatch on the list of
@@ -171,11 +171,10 @@ inference-friendly manner:
 
 Polymorphic built-in functions are handled via automatic specialization of all Haskell type
 variables as types representing PLC type variables, as long as each Haskell variable appears as a
-direct argument to @(->)@ (both possible positions are fine) and not buried somewhere inside
-(i.e. automatic derivation can handle neither @f a@, @ListRep a@, nor @f Int@. Nor is @a -> b@
-allowed to the left of an @(->)@. Where all lower-case names are Haskell type variables).
-We'll call functions having such types "simply-polymorphic".
-See the docs of 'EnumerateFromTo' for details.
+left argument to @(->)@ and is not buried somewhere inside (i.e. automatic derivation can handle
+neither @f a@, @ListRep a@, nor @f Int@. Nor is @a -> b@ allowed to the left of an @(->)@.
+Where all lower-case names are Haskell type variables). We'll call functions having such types
+"simply-polymorphic". See the docs of 'EnumerateFromTo' for details.
 
 The end result is that the user only has to specify the type of the denotation of a built-in
 function and the 'TypeScheme' of the built-in function will be derived automatically. And in the
@@ -302,11 +301,17 @@ instance
 -- by deconstructing @a@ into an applied @(->)@ (we don't recurse to the left of @(->)@, only to the
 -- right) and trying to specialize every argument type as a PLC type variable
 -- (via 'TrySpecializeAsVar') until no deconstruction is possible, at which point we've got a result
--- type which we also try to specialize as a type representing a PLC type variable.
+-- which we don't try to specialize, because that would require an incoherent instance and
+-- introducing one makes code that otherwise type checks perfectly throw errors due to a bug in GHC,
+-- see https://github.com/input-output-hk/plutus/pull/2521#issuecomment-759522445
+-- In practice this means that if the result is a type variable, then this type variable has to
+-- be mentioned as an argument type for inference to work. I.e. @absurd :: Void -> a@ does not get
+-- inferred, since @a@ is only mentioned as the result type and not as an argument type.
+-- But that's a fairly rear use case and we can always provide a type signature manually.
 type EnumerateFromTo :: Nat -> Nat -> GHC.Type -> GHC.Type -> GHC.Constraint
 class EnumerateFromTo i j term a | i term a -> j
-instance {-# INCOHERENT #-} TrySpecializeAsVar i j term a => EnumerateFromTo i j term a
-instance
+instance {-# OVERLAPPABLE #-} i ~ j => EnumerateFromTo i j term a
+instance {-# OVERLAPPING #-}
     ( TrySpecializeAsVar i j term a
     , EnumerateFromTo j k term b
     ) => EnumerateFromTo i k term (a -> b)

plutus-core/test/Evaluation/DynamicBuiltins/Definition.hs

@@ -25,6 +25,7 @@ import           Language.PlutusCore.Constant
 import           Language.PlutusCore.Evaluation.Machine.ExBudgeting
 import           Language.PlutusCore.Evaluation.Machine.ExBudgetingDefaults
 import           Language.PlutusCore.Evaluation.Machine.ExMemory
+import           Language.PlutusCore.Evaluation.Machine.Exception
 import           Language.PlutusCore.Generators.Interesting
 import           Language.PlutusCore.MkPlc                                  hiding (error)
 import           Language.PlutusCore.Pretty
@@ -39,6 +40,7 @@ import           Data.Either
 import qualified Data.Kind                                                  as GHC (Type)
 import           Data.Proxy
 import           Data.Text.Prettyprint.Doc
+import           Data.Void
 import           GHC.Generics
 import           GHC.Ix
 import           Hedgehog                                                   hiding (Opaque, Size, Var)
@@ -108,6 +110,7 @@ data ExtensionFun
     | IdFInteger
     | IdList
     | IdRank2
+    | Absurd
     deriving (Show, Eq, Ord, Enum, Bounded, Ix, Generic, Hashable)
     deriving ExMemoryUsage via (GenericExMemoryUsage ExtensionFun)
 
@@ -133,6 +136,15 @@ instance KnownTypeAst uni a => KnownTypeAst uni (ListRep a) where
     toTypeAst _ = TyApp () Plc.listTy . toTypeAst $ Proxy @a
 type instance ToBinds (ListRep a) = ToBinds a
 
+instance KnownTypeAst uni Void where
+    toTypeAst _ = runQuote $ do
+        a <- freshTyName "a"
+        pure $ TyForall () a (Type ()) $ TyVar () a
+instance KnownType term Void where
+    makeKnown = absurd
+    readKnown = throwingWithCause _UnliftingError "Can't unlift a 'Void'" . Just
+type instance ToBinds Void = '[]
+
 instance (GShow uni, GEq uni, uni `Includes` Integer) => ToBuiltinMeaning uni ExtensionFun where
     type DynamicPart uni ExtensionFun = ()
     type CostingPart uni ExtensionFun = ()
@@ -166,6 +178,12 @@ instance (GShow uni, GEq uni, uni `Includes` Integer) => ToBuiltinMeaning uni Ex
                    )
                 => afa -> afa)
             mempty
+    toBuiltinMeaning Absurd =
+        toStaticBuiltinMeaning
+            (absurd
+                :: a ~ Opaque term (TyVarRep ('TyNameRep "a" 0))
+                => Void -> a)
+            mempty
 
 -- | Check that 'Factorial' from the above computes to the same thing as
 -- a factorial defined in PLC itself.
@@ -299,6 +317,16 @@ test_IdRank2 =
         tyAct @?= tyExp
         typecheckEvaluateCek defBuiltinsRuntimeExt term @?= Right (EvaluationSuccess res)
 
+-- | Test that the type of PLC @Absurd@ is inferred correctly.
+test_Absurd :: TestTree
+test_Absurd =
+    testCase "Absurd" $ do
+        let tyAct = typeOfBuiltinFunction @DefaultUni Absurd
+            tyExp = let a = TyName . Name "a" $ Unique 0
+                        tyForallA = TyForall () a (Type ())
+                    in tyForallA . TyFun () (tyForallA $ TyVar () a) $ TyVar () a
+        tyAct @?= tyExp
+
 test_definition :: TestTree
 test_definition =
     testGroup "definition"
@@ -308,4 +336,5 @@ test_definition =
         , test_IdFInteger
         , test_IdList
         , test_IdRank2
+        , test_Absurd
         ]