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:
- Look at the line
lifting = Sub 'a'
. That's obviously bogus, asChar
s are notDict
s! Yet GHC 8.0.2 and HEAD readily typecheck this code without warnings. - 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
andDict
. All while-fno-defer-type-errors
is enabled!
- 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 |