Runtime loop when using eqT
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.