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 

컴파일러 오류 :

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를 사용하는 것입니다.