CODEWITHSUNDEEP
compiler-errorspurescript
Sridhar Ratnakumar
Sridhar Ratnakumar

Reputation: 85272

PureScript fails to match same constrained types

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.

Upvotes: 1

Views: 224

Answers (1)

Phil Freeman
Phil Freeman

Reputation: 4169

The error message isn't great, but it's not really saying the types aren't unifiable. It's saying that the compiler won't ever attempt to unify constrained types, because passing around the correct dictionaries becomes complicated. So if we get to this point in the type checker, we give up and show this error message instead.

Fortunately, it only arises in very specific situations, involving various interactions between type system features (in this case, records whose field types are polymorphic and involve type classes).

One solution would be to use newtypes instead of type synonyms.

Upvotes: 2

Related Questions