Skip to content

GitLab

  • Projects
  • Groups
  • Snippets
  • Help
    • Loading...
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
  • Sign in / Register
GHC
GHC
  • Project overview
    • Project overview
    • Details
    • Activity
    • Releases
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
    • Locked Files
  • Issues 4,319
    • Issues 4,319
    • List
    • Boards
    • Labels
    • Service Desk
    • Milestones
    • Iterations
  • Merge Requests 355
    • Merge Requests 355
  • Requirements
    • Requirements
    • List
  • CI / CD
    • CI / CD
    • Pipelines
    • Jobs
    • Schedules
  • Security & Compliance
    • Security & Compliance
    • Dependency List
    • License Compliance
  • Operations
    • Operations
    • Incidents
    • Environments
  • Analytics
    • Analytics
    • CI / CD
    • Code Review
    • Insights
    • Issue
    • Repository
    • Value Stream
  • Wiki
    • Wiki
  • Snippets
    • Snippets
  • Members
    • Members
  • Collapse sidebar
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
  • Glasgow Haskell Compiler
  • GHCGHC
  • Issues
  • #18759

Closed
Open
Opened 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
Assignee
Assign to
None
Milestone
None
Assign milestone
Time tracking
None
Due date
None
Reference: ghc/ghc#18759