Types with different forall placements don't unify with QL ImpredicativeTypes
The following program:
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE ImpredicativeTypes #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wall #-}
import GHC.TypeLits
main :: IO ()
main = pure ()
data X = X { x :: forall a. a -> a }
class HasField (name :: Symbol) s a | name s -> a where
getField :: s -> a
instance a ~ (forall x. x -> x) => HasField "x" X a where
getField = x
getX_Ok_sel :: X -> forall a. a -> a
getX_Ok_sel = x
getX_Bad_sel :: forall a. X -> a -> a
getX_Bad_sel = x
getX_Ok_class :: X -> forall a. a -> a
getX_Ok_class = getField @"x"
getX_Bad_class :: forall a. X -> a -> a
getX_Bad_class = getField @"x"
getX_Bad_classUsage :: String
getX_Bad_classUsage = getField @"x" (X id) "hello world"
produces errors with GHC 9.1.0.20200927:
unknown@electronics _build $ ./ghc-stage1 it.hs
[1 of 1] Compiling Main ( it.hs, it.o )
it.hs:29:16: error:
• Couldn't match type: forall a1. a1 -> a1
with: a -> a
Expected: X -> a -> a
Actual: X -> forall a. a -> a
• In the expression: x
In an equation for ‘getX_Bad_sel’: getX_Bad_sel = x
• Relevant bindings include
getX_Bad_sel :: X -> a -> a (bound at it.hs:29:1)
|
29 | getX_Bad_sel = x
| ^
it.hs:35:18: error:
• Couldn't match type: a -> a
with: forall x. x -> x
arising from a use of ‘getField’
• In the expression: getField @"x"
In an equation for ‘getX_Bad_class’: getX_Bad_class = getField @"x"
• Relevant bindings include
getX_Bad_class :: X -> a -> a (bound at it.hs:35:1)
|
35 | getX_Bad_class = getField @"x"
| ^^^^^^^^
it.hs:38:23: error:
• Couldn't match type: String -> String
with: forall x. x -> x
arising from a use of ‘getField’
• In the expression: getField @"x" (X id) "hello world"
In an equation for ‘getX_Bad_classUsage’:
getX_Bad_classUsage = getField @"x" (X id) "hello world"
|
38 | getX_Bad_classUsage = getField @"x" (X id) "hello world"
The Bad_sel
and Bad_class
issues look very similar, but produce error messages with flipped actual and expected types, which confuses me a bit.
Bad_classUsage
looks like a consequence of Bad_class
not working.