Skip to content

GitLab

  • Menu
Projects Groups Snippets
    • Loading...
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
  • Sign in / Register
  • GHC GHC
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
    • Locked Files
  • Issues 4,832
    • Issues 4,832
    • List
    • Boards
    • Service Desk
    • Milestones
    • Iterations
  • Merge requests 450
    • Merge requests 450
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Schedules
    • Test Cases
  • Deployments
    • Deployments
    • Releases
  • Analytics
    • Analytics
    • CI/CD
    • Code review
    • Insights
    • Issue
    • Repository
    • Value stream
  • Wiki
    • Wiki
  • Snippets
    • Snippets
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Glasgow Haskell Compiler
  • GHCGHC
  • Issues
  • #18759

Closed
Open
Created Sep 28, 2020 by Andrzej Rybczak@arybczakContributor

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.

Edited Sep 28, 2020 by Andrzej Rybczak
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking