GitLab

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.