Regression in ambiguity checking for partial type signatures in GHC 9.2
The following program compiles on all GHC versions ranging from 8.6
to 9.0
, but fails on 9.2
and HEAD:
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PartialTypeSignatures #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module PsigBug where
import Data.Kind
( Constraint )
import GHC.TypeLits
( ErrorMessage(..), TypeError )
import GHC.TypeNats ( Nat )
type family OK (i :: Nat) :: Constraint where
OK 1 = ()
OK 2 = ()
OK n = TypeError (ShowType n :<>: Text "is not OK")
class C (i :: Nat) where
foo :: Int
instance C 1 where
foo = 1
instance C 2 where
foo = 2
type family Boo (i :: Nat) :: Nat where
Boo i = i
bar :: Int
bar =
let
quux :: forall (i :: Nat). ( OK (Boo i), _ ) => Int
quux = foo @(Boo i)
in quux @1 + quux @2
PsigBug.hs:38:5: error:
* Could not deduce: OK i0
from the context: (OK (Boo i), C i)
bound by the inferred type for `quux':
forall (i :: Nat). (OK (Boo i), C i) => Int
at PsigBug.hs:38:5-23
* When checking that the inferred type
quux :: forall {i :: Nat}. (OK (Boo i), OK i, C i) => Int
is as general as its (partial) signature
quux :: forall (i :: Nat). (OK (Boo i), C i) => Int
In the expression:
let
quux :: forall (i :: Nat). (OK (Boo i), _) => Int
quux = foo @(Boo i)
in quux @1 + quux @2
In an equation for `bar':
bar
= let
quux :: forall (i :: Nat). (OK (Boo i), _) => Int
quux = foo @(Boo i)
in quux @1 + quux @2
|
38 | quux = foo @(Boo i)
| ^^^^^^^^^^^^^^^^^^^
PsigBug.hs:38:5: error:
* Could not deduce (C i0)
from the context: (OK (Boo i), C i)
bound by the inferred type for `quux':
forall (i :: Nat). (OK (Boo i), C i) => Int
at PsigBug.hs:38:5-23
The type variable `i0' is ambiguous
* When checking that the inferred type
quux :: forall {i :: Nat}. (OK (Boo i), OK i, C i) => Int
is as general as its (partial) signature
quux :: forall (i :: Nat). (OK (Boo i), C i) => Int
In the expression:
let
quux :: forall (i :: Nat). (OK (Boo i), _) => Int
quux = foo @(Boo i)
in quux @1 + quux @2
In an equation for `bar':
bar
= let
quux :: forall (i :: Nat). (OK (Boo i), _) => Int
quux = foo @(Boo i)
in quux @1 + quux @2
|
38 | quux = foo @(Boo i)
| ^^^^^^^^^^^^^^^^^^^
These messages mention an ambiguous variable i0
... but it doesn't actually appear anywhere in the rest of the messages!
This bug prevents one of my libraries from compiling (and I couldn't find a workaround), so this is not only of theoretical interest.