Deferred type error sneaks in with -fno-defer-type-errors enabled

This is a very perplexing bug that MitchellSalad discovered and advertised in this Reddit post. Consider this code:

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# OPTIONS_GHC -fno-defer-type-errors #-}
module Main where

import Data.Coerce (Coercible)
import GHC.Exts (Constraint)
import GHC.TypeLits (Symbol)

data Dict :: Constraint -> * where
  Dict :: a => Dict a

infixr 9 :-
newtype a :- b = Sub (a => Dict b)
instance a => Show (a :- b) where
  showsPrec d (Sub Dict) = showParen (d > 10) $ showString "Sub Dict"

class Lifting p f where
  lifting :: p a :- p (f a)

data Blah a = Blah

newtype J (a :: JType) = J (Blah (J a))
newtype JComparable a = JComparable (J (T (JTy a)))

instance Lifting JReference JComparable where
  lifting = Sub 'a'

class (Coercible a (J (JTy a))) => JReference a where
  type JTy a :: JType

type T a
  = 'Generic ('Iface "java.lang.Comparable") '[a]
data JType = Class Symbol
           | Generic JType [JType]
           | Iface Symbol
type JObject = J (Class "java.lang.Object")
instance JReference JObject where
  type JTy JObject = 'Class "java.lang.Object"

main :: IO ()
main = print (lifting :: JReference JObject :- JReference (JComparable JObject))

There are three concerning things about this:

1. Look at the line lifting = Sub 'a'. That's obviously bogus, as Chars are not Dicts! Yet GHC 8.0.2 and HEAD readily typecheck this code without warnings.
2. So now that we seem to have circumvented type safety, what happens if we actually try to //run// code which uses this bogus Lifting instance? Something truly bizarre, that's what:

$ /opt/ghc/8.0.2/bin/ghci Bug.hs
GHCi, version 8.0.2: http://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Main             ( Bug.hs, interpreted )
Ok, modules loaded: Main.
λ> main
*** Exception: Bug.hs:34:17: error:
    • Couldn't match expected type ‘Dict (JReference (JComparable a))’
                  with actual type ‘Char’
    • In the first argument of ‘Sub’, namely ‘'a'’
      In the expression: Sub 'a'
      In an equation for ‘lifting’: lifting = Sub 'a'
    • Relevant bindings include
        lifting :: JReference a :- JReference (JComparable a)
          (bound at Bug.hs:34:3)
(deferred type error)

Somehow, we managed to defer a type mismatch between Char and Dict. All while -fno-defer-type-errors is enabled!

1. Worst of all, this is a regression from GHC 8.0.1, as it will actually detect the type mismatch at compile-time:

$ /opt/ghc/8.0.1/bin/ghci Bug.hs
GHCi, version 8.0.1: http://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Main             ( Bug.hs, interpreted )

Bug.hs:34:17: error:
    • Couldn't match expected type ‘Dict (JReference (JComparable a))’
                  with actual type ‘Char’
    • In the first argument of ‘Sub’, namely ‘'a'’
      In the expression: Sub 'a'
      In an equation for ‘lifting’: lifting = Sub 'a'
    • Relevant bindings include
        lifting :: JReference a :- JReference (JComparable a)
          (bound at Bug.hs:34:3)

Trac metadata

Trac field	Value
Version	8.0.2
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler (Type checker)
Test case
Differential revisions
BlockedBy
Related
Blocking
CC	MitchellSalad
Operating system
Architecture