Simon Peyton Jones pushed to branch wip/26737 at Glasgow Haskell Compiler / GHC

Commits:

13 changed files:

Changes:

  • compiler/GHC/Builtin/Names.hs
    ... ... @@ -526,7 +526,7 @@ genericTyConNames = [
    526 526
    527 527 
     gHC_PRIM, gHC_PRIM_PANIC,
    528 528 
         gHC_TYPES, gHC_INTERNAL_DATA_DATA, gHC_MAGIC, gHC_MAGIC_DICT,
    529 
    -    gHC_CLASSES, gHC_PRIMOPWRAPPERS :: Module
    529 
    +    gHC_CLASSES, gHC_CLASSES_IP, gHC_PRIMOPWRAPPERS :: Module
    530 530 
     gHC_PRIM           = mkGhcInternalModule (fsLit "GHC.Internal.Prim")   -- Primitive types and values
    531 531 
     gHC_PRIM_PANIC     = mkGhcInternalModule (fsLit "GHC.Internal.Prim.Panic")
    532 532 
     gHC_TYPES          = mkGhcInternalModule (fsLit "GHC.Internal.Types")
    ... ... @@ -534,6 +534,7 @@ gHC_MAGIC = mkGhcInternalModule (fsLit "GHC.Internal.Magic")
    534 534 
     gHC_MAGIC_DICT     = mkGhcInternalModule (fsLit "GHC.Internal.Magic.Dict")
    535 535 
     gHC_CSTRING        = mkGhcInternalModule (fsLit "GHC.Internal.CString")
    536 536 
     gHC_CLASSES        = mkGhcInternalModule (fsLit "GHC.Internal.Classes")
    537 
    +gHC_CLASSES_IP     = mkGhcInternalModule (fsLit "GHC.Internal.Classes.IP")
    537 538 
     gHC_PRIMOPWRAPPERS = mkGhcInternalModule (fsLit "GHC.Internal.PrimopWrappers")
    538 539 
     gHC_INTERNAL_TUPLE = mkGhcInternalModule (fsLit "GHC.Internal.Tuple")
    539 540
    ... ... @@ -1521,7 +1522,7 @@ fromLabelClassOpName
    1521 1522 
     -- Implicit Parameters
    1522 1523 
     ipClassName :: Name
    1523 1524 
     ipClassName
    1524 
    -  = clsQual gHC_CLASSES (fsLit "IP") ipClassKey
    1525 
    +  = clsQual gHC_CLASSES_IP (fsLit "IP") ipClassKey
    1525 1526
    1526 1527 
     -- Overloaded record fields
    1527 1528 
     hasFieldClassName :: Name

  • docs/users_guide/9.16.1-notes.rst
    ... ... @@ -30,6 +30,18 @@ Language
    30 30 
     - The extension :extension:`ExplicitNamespaces` now allows namespace-specified
    31 31 
       wildcards ``type ..`` and ``data ..`` in import and export lists.
    32 32
    33 
    +- Implicit parameters and ``ImpredicativeTypes``.  GHC now knows
    34 
    +  that if ``?foo::S`` is coecible to ``?foo::T`` only if ``S`` is coercible to ``T``.
    35 
    +  Example (from :ghc-ticket:`#26737`)::
    36 
    +
    37 
    +    {-# LANGUAGE ImplicitParams, ImpredicativeTypes #-}
    38 
    +    newtype N = MkN Int
    39 
    +    test :: ((?foo::N) => Bool) -> ((?foo::Int) => Bool)
    40 
    +    test = coerce
    41 
    +
    42 
    +  This is achieved by arranging that ``?foo :: T`` has a representational
    43 
    +  role for ``T``.
    44 
    +
    33 45 
     Compiler
    34 46 
     ~~~~~~~~
    35 47

  • libraries/ghc-internal/ghc-internal.cabal.in
    ... ... @@ -343,6 +343,7 @@ Library
    343 343
    344 344 
             GHC.Internal.CString
    345 345 
             GHC.Internal.Classes
    346 
    +        GHC.Internal.Classes.IP
    346 347 
             GHC.Internal.Debug
    347 348 
             GHC.Internal.Magic
    348 349 
             GHC.Internal.Magic.Dict

  • libraries/ghc-internal/src/GHC/Internal/Classes.hs
    1 1 
     {-# LANGUAGE Trustworthy #-}
    2 2 
     {-# LANGUAGE NoImplicitPrelude, MagicHash, StandaloneDeriving, BangPatterns,
    3 3 
                  KindSignatures, DataKinds, ConstraintKinds,
    4 
    -              MultiParamTypeClasses, FunctionalDependencies #-}
    5 
    -{-# LANGUAGE UnboxedTuples #-}
    6 
    -{-# LANGUAGE AllowAmbiguousTypes #-}
    7 
    -  -- ip :: IP x a => a  is strictly speaking ambiguous, but IP is magic
    4 
    +             MultiParamTypeClasses, FunctionalDependencies,
    5 
    +             UnboxedTuples #-}
    6 
    +
    8 7 
     {-# LANGUAGE UndecidableSuperClasses #-}
    9 8 
       -- Because of the type-variable superclasses for tuples
    10 9
    ... ... @@ -142,6 +141,7 @@ import GHC.Internal.Prim
    142 141 
     import GHC.Internal.Tuple
    143 142 
     import GHC.Internal.CString (unpackCString#)
    144 143 
     import GHC.Internal.Types
    144 
    +import GHC.Internal.Classes.IP
    145 145
    146 146 
     infix  4  ==, /=, <, <=, >=, >
    147 147 
     infixr 3  &&
    ... ... @@ -149,12 +149,6 @@ infixr 2 ||
    149 149
    150 150 
     default ()              -- Double isn't available yet
    151 151
    152 
    --- | The syntax @?x :: a@ is desugared into @IP "x" a@
    153 
    --- IP is declared very early, so that libraries can take
    154 
    --- advantage of the implicit-call-stack feature
    155 
    -class IP (x :: Symbol) a | x -> a where
    156 
    -  ip :: a
    157 
    -
    158 152 
     {- $matching_overloaded_methods_in_rules
    159 153
    160 154 
     Matching on class methods (e.g. @(==)@) in rewrite rules tends to be a bit

  • libraries/ghc-internal/src/GHC/Internal/Classes/IP.hs
    1 
    +{-# LANGUAGE Trustworthy #-}
    2 
    +{-# LANGUAGE NoImplicitPrelude, MagicHash, StandaloneDeriving, BangPatterns,
    3 
    +             KindSignatures, DataKinds, ConstraintKinds,
    4 
    +              MultiParamTypeClasses, FunctionalDependencies #-}
    5 
    +
    6 
    +{-# LANGUAGE AllowAmbiguousTypes, RoleAnnotations, IncoherentInstances #-}
    7 
    +  -- LANGUAGE pragmas: see Note [IP: implicit parameter class]
    8 
    +
    9 
    +{-# OPTIONS_HADDOCK not-home #-}
    10 
    +-----------------------------------------------------------------------------
    11 
    +-- |
    12 
    +-- Module      :  GHC.Internal.Classes.IP
    13 
    +-- Copyright   :  (c) The University of Glasgow, 1992-2002
    14 
    +-- License     :  see libraries/base/LICENSE
    15 
    +--
    16 
    +-- Maintainer  :  ghc-devs@haskell.org
    17 
    +-- Stability   :  internal
    18 
    +-- Portability :  non-portable (GHC extensions)
    19 
    +--
    20 
    +-- Basic classes.
    21 
    +-- Do not import this module directly.  It is an GHC internal only
    22 
    +-- module.  Some of its contents are instead available from @Prelude@
    23 
    +-- and @GHC.Int@.
    24 
    +--
    25 
    +-----------------------------------------------------------------------------
    26 
    +
    27 
    +module GHC.Internal.Classes.IP( IP(..)) where
    28 
    +
    29 
    +import GHC.Internal.Types
    30 
    +
    31 
    +
    32 
    +default ()              -- Double isn't available yet
    33 
    +
    34 
    +-- | The syntax @?x :: a@ is desugared into @IP "x" a@
    35 
    +-- IP is declared very early, so that libraries can take
    36 
    +-- advantage of the implicit-call-stack feature
    37 
    +type role IP nominal representational   -- See (IPRoles)
    38 
    +class IP (x :: Symbol) a | x -> a where
    39 
    +  ip :: a
    40 
    +
    41 
    +{- Note [IP: implicit parameter class]
    42 
    +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    43 
    +An implicit parameter constraint (?foo::ty) is just short for
    44 
    +
    45 
    +   IP "foo" ty
    46 
    +
    47 
    +where ghc-internal:GHC.Internal.Classes.IP is a special class that
    48 
    +GHC knows about, defined in this module.
    49 
    +
    50 
    +* It is a unary type class, with one method `ip`, so it has no cost.
    51 
    +  For example, (?foo::Int) is represented just by an Int.
    52 
    +
    53 
    +* Criticially, it has a functional dependency:
    54 
    +    class IP (x :: Symbol) a | x -> a where ...
    55 
    +  So if we have
    56 
    +    [G] IP "foo" Int
    57 
    +    [W] IP "foo" alpha
    58 
    +  the fundep wil lgive us alpha ~ Int, as desired.
    59 
    +
    60 
    +* The solver has a number of special cases for implicit parameters,
    61 
    +  mainly because a binding  (let ?foo::Int = rhs in body)
    62 
    +  is like a local instance declaration for IP.  Search for uses
    63 
    +  of `isIPClass`.
    64 
    +
    65 
    +Wrinkles
    66 
    +
    67 
    +(IPAmbiguity) The single method of IP has an ambiguous type
    68 
    +      ip :: forall a. IP s a => a
    69 
    +   Hence the LANGUAGE pragama AllowAmbiguousTypes.
    70 
    +   The method `ip` is never called by the user, so ambiguity doesn't matter.
    71 
    +
    72 
    +(IPRoles) IP has a role annotation.  Why?  See #26737.  We want
    73 
    +     [W] IP "foo" t1 ~R# IP "foo" t2
    74 
    +  to decompose to give [W] IP t1 ~R# t2, using /representational/
    75 
    +  equality for (t1 ~R# t2) not nominal.
    76 
    +
    77 
    +  This usually gives a complaint about incoherence, because in general
    78 
    +  (t1 ~R# t2) does NOT imply (C t1) ~R# (C t2) for any normal class.
    79 
    +  But it does for IP, because instance selection is controlled by the Symbol,
    80 
    +  not the type of the payload.  Hence LANGUAGE pragma IncoherentInstances.
    81 
    +  (It is unfortunate that we need a module-wide IncoherentInstances here;
    82 
    +  see #17167.)
    83 
    +
    84 
    +  Side note: arguably this treatment could be applied to any class
    85 
    +  with a functional dependency; but for now we restrict it to IP.
    86 
    +-}
    87 
    +

  • testsuite/tests/interface-stability/base-exports.stdout
    ... ... @@ -3293,6 +3293,7 @@ module GHC.Base where
    3293 3293 
         {-# MINIMAL fmap #-}
    3294 3294 
       type IO :: * -> *
    3295 3295 
       newtype IO a = IO (State# RealWorld -> (# State# RealWorld, a #))
    3296 
    +  type role IP nominal representational
    3296 3297 
       type IP :: Symbol -> * -> Constraint
    3297 3298 
       class IP x a | x -> a where
    3298 3299 
         ip :: a

  • testsuite/tests/interface-stability/base-exports.stdout-mingw32
    ... ... @@ -3293,6 +3293,7 @@ module GHC.Base where
    3293 3293 
         {-# MINIMAL fmap #-}
    3294 3294 
       type IO :: * -> *
    3295 3295 
       newtype IO a = IO (State# RealWorld -> (# State# RealWorld, a #))
    3296 
    +  type role IP nominal representational
    3296 3297 
       type IP :: Symbol -> * -> Constraint
    3297 3298 
       class IP x a | x -> a where
    3298 3299 
         ip :: a

  • testsuite/tests/interface-stability/base-exports.stdout-ws-32
    ... ... @@ -3293,6 +3293,7 @@ module GHC.Base where
    3293 3293 
         {-# MINIMAL fmap #-}
    3294 3294 
       type IO :: * -> *
    3295 3295 
       newtype IO a = IO (State# RealWorld -> (# State# RealWorld, a #))
    3296 
    +  type role IP nominal representational
    3296 3297 
       type IP :: Symbol -> * -> Constraint
    3297 3298 
       class IP x a | x -> a where
    3298 3299 
         ip :: a

  • testsuite/tests/interface-stability/ghc-prim-exports.stdout
    ... ... @@ -1171,6 +1171,7 @@ module GHC.Classes where
    1171 1171 
         (==) :: a -> a -> GHC.Internal.Types.Bool
    1172 1172 
         (/=) :: a -> a -> GHC.Internal.Types.Bool
    1173 1173 
         {-# MINIMAL (==) | (/=) #-}
    1174 
    +  type role IP nominal representational
    1174 1175 
       type IP :: GHC.Internal.Types.Symbol -> * -> Constraint
    1175 1176 
       class IP x a | x -> a where
    1176 1177 
         ip :: a

  • testsuite/tests/interface-stability/ghc-prim-exports.stdout-mingw32
    ... ... @@ -1171,6 +1171,7 @@ module GHC.Classes where
    1171 1171 
         (==) :: a -> a -> GHC.Internal.Types.Bool
    1172 1172 
         (/=) :: a -> a -> GHC.Internal.Types.Bool
    1173 1173 
         {-# MINIMAL (==) | (/=) #-}
    1174 
    +  type role IP nominal representational
    1174 1175 
       type IP :: GHC.Internal.Types.Symbol -> * -> Constraint
    1175 1176 
       class IP x a | x -> a where
    1176 1177 
         ip :: a

  • testsuite/tests/th/TH_implicitParams.stdout
    1 
    -Main.funcToReify :: GHC.Internal.Classes.IP "z"
    2 
    -                                            GHC.Internal.Types.Int =>
    1 
    +Main.funcToReify :: GHC.Internal.Classes.IP.IP "z"
    2 
    +                                               GHC.Internal.Types.Int =>
    3 3 
                         GHC.Internal.Types.Int
    4 4 
     5
    5 5 
     1

  • testsuite/tests/typecheck/should_compile/T26737.hs
    1 
    +{-# LANGUAGE ImpredicativeTypes, ImplicitParams #-}
    2 
    +
    3 
    +module T26737 where
    4 
    +
    5 
    +import Data.Coerce
    6 
    +
    7 
    +newtype Foo = MkFoo Int
    8 
    +
    9 
    +b :: ((?foo :: Foo) => Int) -> ((?foo :: Int) => Int)
    10 
    +b = coerce @(((?foo :: Foo) => Int)) @(((?foo :: Int) => Int))

  • testsuite/tests/typecheck/should_compile/all.T
    ... ... @@ -957,3 +957,4 @@ test('T17705', normal, compile, [''])
    957 957 
     test('T14745', normal, compile, [''])
    958 958 
     test('T26451', normal, compile, [''])
    959 959 
     test('T26582', normal, compile, [''])
    960 
    +test('T26737', normal, compile, [''])

    • —
    View it on GitLab.
    You're receiving this email because of your account on gitlab.haskell.org. Manage all notifications · Help