PureScript не соответствует тем же ограниченным типам

Question

Мне интересно, почему PureScript не может соответствовать двум ограниченным типам, которые являются символами для персонажа, одинаковыми! См. Сообщение об ошибке ниже. Код, который производит это дается непосредственно ниже:

-- 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 ошибка:

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. 

Answer 1

сообщение об ошибке не велика, но это на самом деле не говоря типы не unifiable. Это говорит о том, что компилятор никогда не попытается объединить ограниченные типы, потому что прохождение вокруг правильных словарей становится сложным. Поэтому, если мы доберемся до этой точки проверки типов, мы откажемся и покажем это сообщение об ошибке.

К счастью, он возникает только в особых ситуациях, связанных с различными взаимодействиями между системными функциями типа (в этом случае записи, типы полей которых являются полиморфными и включают классы типов).

Одним из решений было бы использовать newtype s вместо синонимов типов.