[GHC] #13446: Deferred type error sneaks in with -fno-defer-type-errors enabled

[GHC]

#13446: Deferred type error sneaks in with -fno-defer-type-errors enabled
-------------------------------------+-------------------------------------
           Reporter:  RyanGlScott    |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.0.2
  (Type checker)                     |
           Keywords:                 |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  GHC accepts
  Unknown/Multiple                   |  invalid program
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 This is a very perplexing bug that MitchellSalad discovered and advertised
 in
 [https://www.reddit.com/r/haskell/comments/604mze/deferred_type_errors_without_setting/
 this Reddit post]. Consider this code:

 {{{#!hs
 {-# 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
 `Char`s are not `Dict`s! 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!
 3. 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)
 }}}

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/13446>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler