Summary

Use of eqT causes run-time divergence in a weird edge-case.

Steps to reproduce

This example is minimized for simplicity; my actual use case was large and it took me 5 hours to get it down to this:

{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE TypeOperators #-}
import Data.Void
import Data.Typeable
import Data.Type.Equality

class (forall k. k a => k b) => Equ a b

instance Equ a a

data Z' a where
  Z' :: Z' Void

data Z where
  Z :: forall a. Equ Void a => Z' a -> Z

checkZ :: Z -> Bool
checkZ (Z (Z' :: Z' a)) = case eqT of
  Nothing -> False
  Just (Refl :: a :~: Void) -> True

main :: IO ()
main = do
  putStrLn "before..."
  print $ checkZ $ Z Z'
  putStrLn "after!"

Compiles ok. Exe output is:

before...
MinExample: <<loop>>

Expected behavior

This should work and produce

before...
True
after...

Poking around indicates that Eq can propagate along the quantified constraint of Equ, but apparently something magic is happening with Typeable?

Environment

Tested with GHC 8.6 and 8.8 on NixOS.