Opened 5 years ago

Closed 3 years ago

#324 closed defect (worksforme)

Don't display Bot in type error messages

Reported by: benl Owned by:
Priority: normal Milestone: 0.4.3
Component: Core Type Checker Version: 0.3.2
Keywords: Cc:

Description

:set lang Tetra
:set Synth
:load..
module Test with letrec

id [a : Data] (x : a) : a
 = x

thing (blerk : ([a : Data]. a -> a) -> Nat#) : Nat#
 = blerk (\x. x)
;;

Gives

Error loading module
  When checking expression.
    <batch>:50:11
    Type mismatch.
      inferred type: [a : Data].a -> a
      expected type: ?0 -> ?0
    
    with: \(x : Bot). x

Change History (4)

comment:1 Changed 5 years ago by benl

We should also say something about 'cannot infer type' instead of showing raw existentials.

comment:2 Changed 5 years ago by benl

  • Milestone changed from 0.4.1 to 0.4.2

comment:3 Changed 3 years ago by benl

  • Milestone changed from 0.4.2 to 0.4.3

comment:4 Changed 3 years ago by benl

  • Resolution set to worksforme
  • Status changed from new to closed

This particular example works now as we do inference for higher ranked types.

Note: See TracTickets for help on using tickets.