Skip to content

Strange type family unification in `reifyInstances` with 9.4

Summary

Starting with GHC 9.4, reifyInstances unifies a type family constructor against anything else, seemingly treating it as a metavariable.

Steps to reproduce

{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies #-}
module Bug where
import Debug.Trace
import Language.Haskell.TH

-- This empty type family is used to trick GHC into not unifying certain type variables
type family Skolem :: k -> k

class Foo a where
instance Foo Int where
instance Foo (Maybe a) where

bug = do
  a <- newName "a"
  ins <- reifyInstances ''Foo [AppT (ConT ''Skolem) (VarT a)]
  mapM_ traceShowM ins
  pure []
{-# LANGUAGE TemplateHaskell #-}
module Main where
import Bug

$(bug)

main = pure ()

Running the above Main module with GHC 9.2 produces empty output. With GHC 9.4 (and 9.6, and 9.7.20230527), it produces the following:

InstanceD Nothing [] (AppT (ConT Bug.Foo) (SigT (AppT (ConT GHC.Maybe.Maybe) (VarT a_7566047373982442759)) StarT)) []

Only the Foo (Maybe a) instance is returned, as if I had asked for Foo (f a) instead of Foo (Skolem a).

Expected behavior

Return no instances.

Context

https://github.com/obsidiansystems/dependent-sum-template/pull/2#issuecomment-1649439589

Environment

  • GHC version used: 9.4.5
  • Operating System: NixOS
  • System Architecture: x86_64-linux
Edited by Naïm Favier
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information