Type family equality gets stuck on types that fail the occurs check
Summary
A type family that should check two types for equality gets stuck, even though their equality would fail the occurs check.
Steps to reproduce
The following program doesn't compile:
{-# LANGUAGE AllowAmbiguousTypes #-}
module Occurs where
import Data.Functor.Identity
import Data.Proxy
type family Equal a b where
Equal a a = 'True
Equal a b = 'False
foo :: Proxy (Equal (Identity a) a) -> Proxy 'False
foo = id
with error:
• Couldn't match type ‘Equal (Identity a) a’ with ‘'False’
Expected type: Proxy (Equal (Identity a) a) -> Proxy 'False
Actual type: Proxy 'False -> Proxy 'False
• In the expression: id
In an equation for ‘foo’: foo = id
• Relevant bindings include
foo :: Proxy (Equal (Identity a) a) -> Proxy 'False
(bound at /home/sandy/Vikrem.hs:14:1)
|
14 | foo = id
|
The Equal
type family is stuck due to a
being a variable, but the only way Equal (Identity a) a ~ 'True
is for an infinite instantiation of a
. As such, this thing should reduce.
Expected behavior
I expect the above program to compile, with Equal (Identity a) a
reducing to 'False
.
Environment
- GHC version used: 8.6.5
Optional:
- Operating System: Archlinux
- System Architecture: x86_64