Opened 3 years ago

Last modified 17 months ago

#386 new feature

Better inference when case alternatives have differing effects.

Reported by: benl Owned by:
Priority: normal Milestone:
Component: Source Typing Version: 0.4.2
Keywords: Cc:

Description

Emmitting the sig for 'loop' causes the checker to complain that S Pure Bool does not match S (Read r) Bool. We should have enough information for the sig not to be needed.

-- | Check if the given number is a multiple of any
--   of the others in an array.
check   (primes: Array r Nat)   -- ^ Array of primes.
        (len: Nat)              -- ^ Length of array.
        (val: Nat)              -- ^ Value to check.
        : S (Read r) Bool
 = loop 0
 where  
        loop (ix: Nat): S (Read r) Bool
         | ix >= len    = False
         | rem# val (readArray primes ix) == 0  
                        = True
         | otherwise    = loop (ix + 1)

Change History (3)

comment:1 Changed 3 years ago by benl

  • Milestone changed from 0.4.3 to 0.5.0
  • Summary changed from In defib/primes test work out why we need a local type sig for the 'loop' to Better inference when case alternatives have differing effects.
  • Type changed from defect to enhancement

comment:2 Changed 2 years ago by benl

  • Milestone 0.5.0 deleted

comment:3 Changed 17 months ago by benl

  • Component changed from Core Type Checker to Source Typing
  • Type changed from enhancement to feature
Note: See TracTickets for help on using tickets.