Re: CI Status Update

[Ben Gamari]

Ben Gamari  writes:

> Hi all,
>
Hi all,

At this point CI should be fully functional on the stable and master
branches again. However, do note that older base commits may refer to
Docker images that are sadly no longer available. Such cases can be
resolved by simply rebasing.

Cheers,

- Ben



signature.asc
Description: PGP signature
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Re: Error message degradation for (<= :: Nat -> Nat -> Constraint) in GHC 9.2+

[Christiaan Baaij]

I have reported the issue here:
https://gitlab.haskell.org/ghc/ghc/-/issues/20009

On Thu, 17 Jun 2021 at 18:44, Simon Peyton Jones 
wrote:

> Christiaan,
>
>
>
> Do please submit a bug report on GHC’s issue tracker, with a way to
> reproduce it.
>
>
>
> Thanks
>
>
> Simon
>
>
>
> *From:* ghc-devs  *On Behalf Of *Christiaan
> Baaij
> *Sent:* 17 June 2021 10:44
> *To:* ghc-devs 
> *Subject:* Error message degradation for (<= :: Nat -> Nat -> Constraint)
> in GHC 9.2+
>
>
>
> Hi Ghc-Devs,
>
>
>
> When upgrading one of our tc plugins
> https://hackage.haskell.org/package/ghc-typelits-natnormalise
> 
> to GHC 9.2, one of our tests, repeated here:
>
> ```
>
> {-# LANGUAGE DataKinds, TypeFamilies, TypeOperators #-}
> module TestInEq where
>
> import Data.Proxy
> import GHC.TypeLits
>
> proxyInEq :: (a <= b) => Proxy a -> Proxy b -> ()
> proxyInEq _ _ = ()
>
> proxyInEq1 :: Proxy a -> Proxy (a+1) -> ()
> proxyInEq1 = proxyInEq
> ```
>
>
>
> degraded quite badly in terms of the error message.
>
> Where in GHC 9.0.1 we get:
>
>
>
> ```
>
> TestInEq.hs:11:14: error:
> • Couldn't match type ‘a <=? (a + 1)’ with ‘'True’
> arising from a use of ‘proxyInEq’
> • In the expression: proxyInEq
>   In an equation for ‘proxyInEq1’: proxyInEq1 = proxyInEq
> • Relevant bindings include
> proxyInEq1 :: Proxy a -> Proxy (a + 1) -> ()
>   (bound at TestInEq.hs:11:1)
>|
> 11 | proxyInEq1 = proxyInEq
>|
>
> ```
>
>
>
> with GHC 9.2.0.20210422 we get:
>
>
>
> ```
>
> TestInEq.hs:11:14: error:
> • Couldn't match type ‘Data.Type.Ord.OrdCond
>  (CmpNat a (a + 1)) 'True 'True 'False’
>  with ‘'True’
> arising from a use of ‘proxyInEq’
> • In the expression: proxyInEq
>   In an equation for ‘proxyInEq1’: proxyInEq1 = proxyInEq
> • Relevant bindings include
> proxyInEq1 :: Proxy a -> Proxy (a + 1) -> ()
>   (bound at TestInEq.hs:11:1)
>|
> 11 | proxyInEq1 = proxyInEq
>|
> ```
>
>
>
> Errors messages involving type-level naturals and their operations already
> weren't the poster-child of comprehensable GHC error messages, but this
> change has made the situation worse in my opinion.
>
>
>
> This change in error message is due to:
> https://gitlab.haskell.org/ghc/ghc/-/commit/eea96042f1e8682605ae68db10f2bcdd7dab923e
> 
>
>
>
> Is there a way we can get the nicer pre-9.2.0.2021 error message again
> before the proper 9.2.1 release?
>
> e.g. by doing one of the following:
>
> 1. Reinstate `(<=? :: Nat -> Nat -> Bool)` as a builtin type family
>
> 2. Somehow add a custom type-error to `Data.Type.Ord.OrdCond`
>
> 3. Don't expand type aliases in type errors
>
>
>
> What do you think? should this be fixed? should this be fixed before the
> 9.2.1 release?
>
>
>
> -- Christiaan
>
>
>
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

RE: Error message degradation for (<= :: Nat -> Nat -> Constraint) in GHC 9.2+

[Simon Peyton Jones via ghc-devs]

Christiaan,

Do please submit a bug report on GHC's issue tracker, with a way to reproduce 
it.

Thanks

Simon

From: ghc-devs  On Behalf Of Christiaan Baaij
Sent: 17 June 2021 10:44
To: ghc-devs 
Subject: Error message degradation for (<= :: Nat -> Nat -> Constraint) in GHC 
9.2+

Hi Ghc-Devs,

When upgrading one of our tc plugins 
https://hackage.haskell.org/package/ghc-typelits-natnormalise
 to GHC 9.2, one of our tests, repeated here:

```
{-# LANGUAGE DataKinds, TypeFamilies, TypeOperators #-}
module TestInEq where

import Data.Proxy
import GHC.TypeLits

proxyInEq :: (a <= b) => Proxy a -> Proxy b -> ()
proxyInEq _ _ = ()

proxyInEq1 :: Proxy a -> Proxy (a+1) -> ()
proxyInEq1 = proxyInEq
```

degraded quite badly in terms of the error message.
Where in GHC 9.0.1 we get:

```
TestInEq.hs:11:14: error:
* Couldn't match type 'a <=? (a + 1)' with ''True'
arising from a use of 'proxyInEq'
* In the expression: proxyInEq
  In an equation for 'proxyInEq1': proxyInEq1 = proxyInEq
* Relevant bindings include
proxyInEq1 :: Proxy a -> Proxy (a + 1) -> ()
  (bound at TestInEq.hs:11:1)
   |
11 | proxyInEq1 = proxyInEq
   |
```

with GHC 9.2.0.20210422 we get:

```
TestInEq.hs:11:14: error:
* Couldn't match type 'Data.Type.Ord.OrdCond
 (CmpNat a (a + 1)) 'True 'True 'False'
 with ''True'
arising from a use of 'proxyInEq'
* In the expression: proxyInEq
  In an equation for 'proxyInEq1': proxyInEq1 = proxyInEq
* Relevant bindings include
proxyInEq1 :: Proxy a -> Proxy (a + 1) -> ()
  (bound at TestInEq.hs:11:1)
   |
11 | proxyInEq1 = proxyInEq
   |
```

Errors messages involving type-level naturals and their operations already 
weren't the poster-child of comprehensable GHC error messages, but this change 
has made the situation worse in my opinion.

This change in error message is due to: 
https://gitlab.haskell.org/ghc/ghc/-/commit/eea96042f1e8682605ae68db10f2bcdd7dab923e

Is there a way we can get the nicer pre-9.2.0.2021 error message again before 
the proper 9.2.1 release?
e.g. by doing one of the following:
1. Reinstate `(<=? :: Nat -> Nat -> Bool)` as a builtin type family
2. Somehow add a custom type-error to `Data.Type.Ord.OrdCond`
3. Don't expand type aliases in type errors

What do you think? should this be fixed? should this be fixed before the 9.2.1 
release?

-- Christiaan

___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Re: Error message degradation for (<= :: Nat -> Nat -> Constraint) in GHC 9.2+

[Carter Schonwald]

Agreed and better articulated than what I likely would have said

On Thu, Jun 17, 2021 at 8:38 AM Sam Derbyshire 
wrote:

> Hi Christiaan,
>
> As far as I'm concerned that's a worrying regression, and I think you
> should file a ticket on the GHC tracker about it.
> I believe GHC already contains logic to avoid expanding type synonyms in
> error messages in certain situations, but it apparently doesn't apply here.
> Hopefully someone more knowledgeable about this can chime in.
>
> Sam
> ___
> ghc-devs mailing list
> ghc-devs@haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Re: Error message degradation for (<= :: Nat -> Nat -> Constraint) in GHC 9.2+

[Christiaan Baaij]

I imagined solution 1. as:

1. reinstate the magic type family `(<=?) :: Nat -> Nat -> Bool` in
GHC.TypeNats
```
module GHC.TypeNats where

type family (m :: Nat) <=? (n :: Nat) :: Bool
```

2. instead of exporting the following type alias from Data.Type.Ord
```
type (<=?) :: k -> k -> Bool
type m <=? n = OrdCond (Compare m n) 'True 'True 'False
```

do:

```
import qualified GHC.TypeNats as T

type (<=?) :: forall k . k -> k -> Bool
type family (<=?) a b where
  (<=?) (a :: T.Nat) b = (T.<=?) a b
  (<=?) a b= OrdCond (Compare a b) 'True 'True 'False
```

I realize this is far from ideal

On Thu, 17 Jun 2021 at 14:46, Adam Gundry  wrote:

> Hi Christiaan,
>
>
> On 17/06/2021 10:43, Christiaan Baaij wrote:
> > [...]
> >
> > Errors messages involving type-level naturals and their operations
> > already weren't the poster-child of comprehensable GHC error messages,
> > but this change has made the situation worse in my opinion.
> >
> > This change in error message is due to:
> >
> https://gitlab.haskell.org/ghc/ghc/-/commit/eea96042f1e8682605ae68db10f2bcdd7dab923e
> > <
> https://gitlab.haskell.org/ghc/ghc/-/commit/eea96042f1e8682605ae68db10f2bcdd7dab923e
> >
> >
> > Is there a way we can get the nicer pre-9.2.0.2021 error message again
> > before the proper 9.2.1 release?
> > e.g. by doing one of the following:
> > 1. Reinstate `(<=? :: Nat -> Nat -> Bool)` as a builtin type family
> > 2. Somehow add a custom type-error to `Data.Type.Ord.OrdCond`
> > 3. Don't expand type aliases in type errors
> >
> > What do you think? should this be fixed? should this be fixed before the
> > 9.2.1 release?
>
> I don't know the context for this change or the immediate feasibility of
> 1, but regarding the other two points:
>
> GHC does in general try to avoid expanding type aliases if it doesn't
> need to (but it does expand type families). The difficulty here is that
> the constraint solver must expand the synonym to see if the constraint
> can be solved, and it seems hard (though perhaps not impossible) to keep
> track of the original forms of constraints as they get simplified by the
> solver.
>
> Presumably it wouldn't be terribly difficult to add some built-in magic
> to GHC's error message printing machinery that looked through types for
> occurrences of specific patterns (like OrdCond with concrete arguments)
> and replaced them with simpler versions. It would be really nice,
> though, to have a way to specify this as a user, rather than it being
> limited to built-in magic.
>
> I'm imagining having a pragma to mark type synonyms as "contractible",
> then when showing a type, GHC would try to match it against the RHSs of
> contractible synonyms in scope. If there are multiple matches, probably
> it should pick the most specific; I'm not sure if we should have some
> other mechanism for prioritization or if we should just accept arbitrary
> choices where there is overlap.
>
> Does this sound useful to others? I think it could be really helpful for
> improving type error messages. It won't be in 9.2 though...
>
> Best wishes,
>
> Adam
>
>
> --
> Adam Gundry, Haskell Consultant
> Well-Typed LLP, https://www.well-typed.com/
>
> Registered in England & Wales, OC335890
> 118 Wymering Mansions, Wymering Road, London W9 2NF, England
>
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Re: Error message degradation for (<= :: Nat -> Nat -> Constraint) in GHC 9.2+

[Adam Gundry]

Hi Christiaan,


On 17/06/2021 10:43, Christiaan Baaij wrote:
> [...]
> 
> Errors messages involving type-level naturals and their operations
> already weren't the poster-child of comprehensable GHC error messages,
> but this change has made the situation worse in my opinion.
> 
> This change in error message is due to:
> https://gitlab.haskell.org/ghc/ghc/-/commit/eea96042f1e8682605ae68db10f2bcdd7dab923e
> 
> 
> Is there a way we can get the nicer pre-9.2.0.2021 error message again
> before the proper 9.2.1 release?
> e.g. by doing one of the following:
> 1. Reinstate `(<=? :: Nat -> Nat -> Bool)` as a builtin type family
> 2. Somehow add a custom type-error to `Data.Type.Ord.OrdCond`
> 3. Don't expand type aliases in type errors
> 
> What do you think? should this be fixed? should this be fixed before the
> 9.2.1 release?

I don't know the context for this change or the immediate feasibility of
1, but regarding the other two points:

GHC does in general try to avoid expanding type aliases if it doesn't
need to (but it does expand type families). The difficulty here is that
the constraint solver must expand the synonym to see if the constraint
can be solved, and it seems hard (though perhaps not impossible) to keep
track of the original forms of constraints as they get simplified by the
solver.

Presumably it wouldn't be terribly difficult to add some built-in magic
to GHC's error message printing machinery that looked through types for
occurrences of specific patterns (like OrdCond with concrete arguments)
and replaced them with simpler versions. It would be really nice,
though, to have a way to specify this as a user, rather than it being
limited to built-in magic.

I'm imagining having a pragma to mark type synonyms as "contractible",
then when showing a type, GHC would try to match it against the RHSs of
contractible synonyms in scope. If there are multiple matches, probably
it should pick the most specific; I'm not sure if we should have some
other mechanism for prioritization or if we should just accept arbitrary
choices where there is overlap.

Does this sound useful to others? I think it could be really helpful for
improving type error messages. It won't be in 9.2 though...

Best wishes,

Adam


-- 
Adam Gundry, Haskell Consultant
Well-Typed LLP, https://www.well-typed.com/

Registered in England & Wales, OC335890
118 Wymering Mansions, Wymering Road, London W9 2NF, England
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Re: Error message degradation for (<= :: Nat -> Nat -> Constraint) in GHC 9.2+

[Sam Derbyshire]

Hi Christiaan,

As far as I'm concerned that's a worrying regression, and I think you
should file a ticket on the GHC tracker about it.
I believe GHC already contains logic to avoid expanding type synonyms in
error messages in certain situations, but it apparently doesn't apply here.
Hopefully someone more knowledgeable about this can chime in.

Sam
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Error message degradation for (<= :: Nat -> Nat -> Constraint) in GHC 9.2+

[Christiaan Baaij]

Hi Ghc-Devs,

When upgrading one of our tc plugins
https://hackage.haskell.org/package/ghc-typelits-natnormalise to GHC 9.2,
one of our tests, repeated here:

```
{-# LANGUAGE DataKinds, TypeFamilies, TypeOperators #-}
module TestInEq where

import Data.Proxy
import GHC.TypeLits

proxyInEq :: (a <= b) => Proxy a -> Proxy b -> ()
proxyInEq _ _ = ()

proxyInEq1 :: Proxy a -> Proxy (a+1) -> ()
proxyInEq1 = proxyInEq
```

degraded quite badly in terms of the error message.
Where in GHC 9.0.1 we get:

```
TestInEq.hs:11:14: error:
• Couldn't match type ‘a <=? (a + 1)’ with ‘'True’
arising from a use of ‘proxyInEq’
• In the expression: proxyInEq
  In an equation for ‘proxyInEq1’: proxyInEq1 = proxyInEq
• Relevant bindings include
proxyInEq1 :: Proxy a -> Proxy (a + 1) -> ()
  (bound at TestInEq.hs:11:1)
   |
11 | proxyInEq1 = proxyInEq
   |
```

with GHC 9.2.0.20210422 we get:

```
TestInEq.hs:11:14: error:
• Couldn't match type ‘Data.Type.Ord.OrdCond
 (CmpNat a (a + 1)) 'True 'True 'False’
 with ‘'True’
arising from a use of ‘proxyInEq’
• In the expression: proxyInEq
  In an equation for ‘proxyInEq1’: proxyInEq1 = proxyInEq
• Relevant bindings include
proxyInEq1 :: Proxy a -> Proxy (a + 1) -> ()
  (bound at TestInEq.hs:11:1)
   |
11 | proxyInEq1 = proxyInEq
   |
```

Errors messages involving type-level naturals and their operations already
weren't the poster-child of comprehensable GHC error messages, but this
change has made the situation worse in my opinion.

This change in error message is due to:
https://gitlab.haskell.org/ghc/ghc/-/commit/eea96042f1e8682605ae68db10f2bcdd7dab923e

Is there a way we can get the nicer pre-9.2.0.2021 error message again
before the proper 9.2.1 release?
e.g. by doing one of the following:
1. Reinstate `(<=? :: Nat -> Nat -> Bool)` as a builtin type family
2. Somehow add a custom type-error to `Data.Type.Ord.OrdCond`
3. Don't expand type aliases in type errors

What do you think? should this be fixed? should this be fixed before the
9.2.1 release?

-- Christiaan
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Re: Rewriting plugins: request for feedback

[Christiaan Baaij]

Hi Sam,

Thanks for picking this up, the API looks good so far.
I'll try to port our https://hackage.haskell.org/package/ghc-typelits-extra
package to the new API.

Though first I need to upgrade
https://hackage.haskell.org/package/ghc-typelits-natnormalise to the GHC
9.2+ API,
which is got somewhat more complicated than usual GHC upgrades due to a
change in representation of (<=? :: Nat -> Nat -> Bool) in
https://gitlab.haskell.org/ghc/ghc/-/commit/eea96042f1e8682605ae68db10f2bcdd7dab923e

I'll report back any issues I encounter if/when I encounter any.

Cheers,

Christiaan


On Wed, 16 Jun 2021 at 23:04, Sam Derbyshire 
wrote:

> Hey everyone,
>
> I've put up some haddocks for this new type-checking plugin API, see here:
> https://sheaf.github.io/ghc-tcplugin-api/GHC-TcPlugin-API.html.
> (The page is mainly meant to be navigated using the contents pane.)
>
> I hope this might be a more welcoming point of entry for people who are
> interested in learning about GHC typechecker plugins.
>
> Let me know what you think,
>
> Thanks,
>
> Sam
> ___
> ghc-devs mailing list
> ghc-devs@haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs