GitLab

Summary

Write a brief description of the issue.

Steps to reproduce

Create a file foo.hs with the code

{-# OPTIONS_GHC -cpp -XMagicHash #-}
{- For Hugs, use the option -F"cpp -P -traditional" -}

module Main where

import qualified Prelude

#ifdef __GLASGOW_HASKELL__
import qualified GHC.Base
#else
-- HUGS
import qualified IOExts
#endif

#ifdef __GLASGOW_HASKELL__
type Any = GHC.Base.Any
#else
-- HUGS
type Any = ()
#endif

data Type base_type =
   Base base_type
 | Arrow (Type base_type) (Type base_type)

type Interp base_type base_interp = Any

data Type0 base_type =
   Type_base base_type
 | Prod (Type0 base_type) (Type0 base_type)
 | List (Type0 base_type)
 | Option (Type0 base_type)
 | Unit

type Interp0 base base_interp = Any

type ExprInfoT =
  (Type (Type0 Any)) -> Any -> Interp (Type0 Any) (Interp0 Any Any)
  -- singleton inductive, whose constructor was Build_ExprInfoT

type Base0 = Any

type Ident = Any

type Base_interp = Any

ident_interp :: ExprInfoT -> (Type (Type0 Base0)) -> Ident -> Interp (Type0 Base0) (Interp0 Base0 Base_interp)
ident_interp exprInfoT =
  exprInfoT

seq :: a1 -> a2 -> a2
seq _ y =
  y

main :: GHC.Base.IO ()
main =
  seq ident_interp (GHC.Base.return ())

Run ghc foo.hs -o foo with ghc 9.0.1 (executed on GH Actions here) and note that it completes fine. Run the same command with ghc 9.2.1 (executed on GH Actions here and note that it errors with

foo.hs:37:1: error:
Error:     • Uninferrable type variables k0, k1, k2 in
      the type synonym right-hand side:
      Type (Type0 (Any @{*}))
      -> Any @{*}
      -> Interp
           @{*}
           @{*}
           @{k0}
           (Type0 (Any @{*}))
           (Interp0 @{k0} @{k1} @{k2} (Any @{k1}) (Any @{k2}))
    • In the type declaration for ‘ExprInfoT’
   |
37 | type ExprInfoT =
   | ^^^^^^^^^^^^^^^^...

Expected behavior

I expect code that compiles fine in 9.0.1 to continue compiling fine in 9.2.1. If this is not supposed to work, then Coq needs to be updated so that it can extract code compatible with Haskell 9.2.1 (see coq/coq#15180)

Environment

• GHC version used: 9.2.1 (failing), 9.0.1 (succeeding)

Optional:

• Operating System: Linux
• System Architecture: