Regression: HEAD fails to typecheck uses of (GHC.TypeNats.<=) that 9.0.1 could
Originally observed on a head.hackage
build here.
The constraints
library fails to compile with HEAD. Here is a minimized example of what goes wrong:
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Bug where
import Data.Kind
import Data.Type.Bool
import GHC.TypeNats
data Dict :: Constraint -> Type where
Dict :: c => Dict c
type family Min (m::Nat) (n::Nat) :: Nat where
Min m n = If (n <=? m) n m
type family Max (m::Nat) (n::Nat) :: Nat where
Max m n = If (n <=? m) m n
eqLe :: (a ~ b) => Dict (a <= b)
eqLe = Dict
minZero :: Dict (Min n 0 ~ 0)
minZero = Dict
maxZero :: Dict (Max n 0 ~ n)
maxZero = Dict
zeroLe :: Dict (0 <= a)
zeroLe = Dict
leId :: Dict (a <= a)
leId = Dict
This compiles with GHC 9.0.1, but with HEAD it errors thusly:
$ ~/Software/ghc-9.1.20210303/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:22:9: error:
• Couldn't match type: Data.Type.Ord.OrdCond
(Data.Type.Ord.Compare b0 b0) 'True 'True 'False
with: Data.Type.Ord.OrdCond
(Data.Type.Ord.Compare b b) 'True 'True 'False
Expected: Dict (a <= b)
Actual: Dict (b0 <= b0)
NB: ‘Data.Type.Ord.OrdCond’ is a non-injective type family
The type variable ‘b0’ is ambiguous
• In the ambiguity check for ‘eqLe’
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
In the type signature: eqLe :: (a ~ b) => Dict (a <= b)
|
22 | eqLe :: (a ~ b) => Dict (a <= b)
| ^^^^^^^^^^^^^^^^^^^^^^^^
Bug.hs:25:12: error:
• Couldn't match type: If
(Data.Type.Ord.OrdCond (CmpNat 0 n0) 'True 'True 'False) 0 n0
with: If
(Data.Type.Ord.OrdCond (CmpNat 0 n) 'True 'True 'False) 0 n
Expected: Dict (Min n 0 ~ 0)
Actual: Dict (Min n0 0 ~ 0)
NB: ‘If’ is a non-injective type family
The type variable ‘n0’ is ambiguous
• In the ambiguity check for ‘minZero’
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
In the type signature: minZero :: Dict (Min n 0 ~ 0)
|
25 | minZero :: Dict (Min n 0 ~ 0)
| ^^^^^^^^^^^^^^^^^^
Bug.hs:31:11: error:
• Couldn't match type: Data.Type.Ord.OrdCond
(CmpNat 0 a0) 'True 'True 'False
with: Data.Type.Ord.OrdCond (CmpNat 0 a) 'True 'True 'False
Expected: Dict (0 <= a)
Actual: Dict (0 <= a0)
NB: ‘Data.Type.Ord.OrdCond’ is a non-injective type family
The type variable ‘a0’ is ambiguous
• In the ambiguity check for ‘zeroLe’
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
In the type signature: zeroLe :: Dict (0 <= a)
|
31 | zeroLe :: Dict (0 <= a)
| ^^^^^^^^^^^^^
Bug.hs:34:9: error:
• Couldn't match type: Data.Type.Ord.OrdCond
(Data.Type.Ord.Compare a0 a0) 'True 'True 'False
with: Data.Type.Ord.OrdCond
(Data.Type.Ord.Compare a a) 'True 'True 'False
Expected: Dict (a <= a)
Actual: Dict (a0 <= a0)
NB: ‘Data.Type.Ord.OrdCond’ is a non-injective type family
The type variable ‘a0’ is ambiguous
• In the ambiguity check for ‘leId’
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
In the type signature: leId :: Dict (a <= a)
|
34 | leId :: Dict (a <= a)
| ^^^^^^^^^^^^^
It looks like commit eea96042 (Add cmpNat, cmpSymbol, and cmpChar
) is the culprit. It's unclear to me if this is expected behavior, however. Since the commit lacks a changelog entry, I'm unclear if this was anticipated or not.