I'm wondering why PureScript is unable to match two constrained types that are, character to character, the same! See the error message further below. The code that produces it is given immediately below:
-- We are using https://pursuit.purescript.org/packages/purescript-sized-vectors/1.0.0
import Data.Typelevel.Num (class Lt, class Nat, D2, D7)
import Data.Vec (Vec, modifyAt)
import Prelude (($))
newtype FixedMatrix72 a = FixedMatrix72 (Vec D2 (Vec D7 a))
type Row = forall n. (Nat n, Lt n D2) => n
type Col = forall n. (Nat n, Lt n D7) => n
newtype Ref = Ref { row :: Row, col :: Col }
-- Compiler error is for this function
modify :: forall a. Ref -> (a -> a) -> FixedMatrix72 a -> FixedMatrix72 a
modify (Ref ref) f (FixedMatrix72 m) =
FixedMatrix72 $ modifyAt ref.row (modifyAt ref.col f) m
Compiler error:
Could not match constrained type
( Nat t0
, Lt t0 D2
) => t0
with type
( Nat t0
, Lt t0 D2
) => t0
while trying to match type ( Nat t0
, Lt t0 D2
) => t0
with type ( Nat t0
, Lt t0 D2
) => t0
while solving type class constraint
Data.Typelevel.Num.Ops.Lt (( Nat t0
, Lt t0 D2
) => t0
)
D2
while checking that expression \$0 ->
\f ->
\$1 ->
case $0 f $1 of
...
has type forall a. Ref -> (a -> a) -> FixedMatrix72 a -> FixedMatrix72 a
in value declaration modify
where t0 is an unknown type
See https://github.com/purescript/purescript/wiki/Error-Code-ConstrainedTypeUnified for more information,
or to contribute content related to this error.