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