Skip to content

  • Projects
  • Groups
  • Snippets
  • Help
    • Loading...
    • Help
    • Support
    • Submit feedback
  • Sign in / Register
GHC
GHC
  • Project
    • Project
    • Details
    • Activity
    • Releases
    • Cycle Analytics
    • Insights
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
    • Charts
    • Locked Files
  • Issues 3,625
    • Issues 3,625
    • List
    • Boards
    • Labels
    • Milestones
  • Merge Requests 198
    • Merge Requests 198
  • CI / CD
    • CI / CD
    • Pipelines
    • Jobs
    • Schedules
    • Charts
  • Security & Compliance
    • Security & Compliance
    • Dependency List
  • Wiki
    • Wiki
  • Snippets
    • Snippets
  • Members
    • Members
  • Collapse sidebar
  • Activity
  • Graph
  • Charts
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
  • Glasgow Haskell Compiler
  • GHCGHC
  • Issues
  • #17458

Closed
Open
Opened Nov 09, 2019 by Max Harms@Raelifin
  • Report abuse
  • New issue
Report abuse New issue

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.

Edited Nov 09, 2019 by Ben Gamari

Related issues

  • Discussion
  • Designs
Assignee
Assign to
None
Milestone
None
Assign milestone
Time tracking
None
Due date
None
5
Labels
bug incorrect runtime result P::normal QuantifiedConstraints Typeable
Assign labels
  • View project labels
Reference: ghc/ghc#17458