Home - News ( United States | United Kingdom | Italy | Germany ) - Football scores

Showing content from https://github.com/agda/agda/issues/6657 below:

Turn `--guardedness` warning into an error-hint · Issue #6657 · agda/agda · GitHub

On Agda v2.6.3-b499d12, the --guardedness warning is displayed for files declaring a coinductive record without the --guardedness flag.

This warning doesn't work well with libraries.

I have three agda files, one library (Lib) and two clients, Ex1 and Ex2:

module Lib where

    open import Agda.Builtin.String
    open import Agda.Builtin.Unit

    data Cmd : Set where
        print : String → Cmd
        exit : Cmd

    data ⊥ : Set where -- empty type

    cmd-ret-ty : Cmd → Set
    cmd-ret-ty (print _) = ⊤
    cmd-ret-ty exit = ⊥

    record ITree : Set where
        coinductive
        constructor _>>=_
        field head : Cmd
        field tail : (cmd-ret-ty head) → ITree

    _>>_ : Cmd → ITree → ITree
    c >> t = c >>= λ _ → t
    {-# INLINE _>>_ #-}

module Ex1 where

    open import Lib

    hello : ITree
    hello = do
        print "Hello"
        print "World"
        () ← exit

module Ex2 where

    open import Lib
    open ITree

    loop : ITree
    loop .head = print "Hello"
    loop .tail _ = do
        print "World"
        loop

Note that Ex2 requires the --guardedness option to pass termination checking, but Lib and Ex1 do not.

I am trying to design the library Lib such that:

• Clients do not see spurious warnings (i.e. the "please enable --guardedness" warning should not be shown in Ex1)
• Clients only pay for the pragmas they need (i.e. {-# OPTIONS --guardedness #-} is OK in Ex2 but should not be mandatory in Ex1)
• Clients get helpful warnings (i.e. the "please enable --guardedness" warning should be shown in Ex2)

Here are the combinations of pragmas I have tried:

1. No options in Lib or Ex1, {-# OPTIONS --guardedness #-} in Ex2:
   • Ex1 displays the --guardedness warning (🙁)
   • Ex2 passes without warnings (✅)
2. {-# OPTIONS --guardedness #-} in Lib and Ex1 and Ex2
   • Ex1 passes without warnings (✅), but needs an extra pragma (🙁)
   • Ex2 passes without warnings (✅)
3. {-# OPTIONS -W noNoGuardednessFlag #-} in Lib, no options in Ex1, {-# OPTIONS --guardedness #-} in Ex2:
   • Ex1 passes without warnings (✅), and no extra pragma (✅)
   • Ex2 passes without warnings (✅)
4. {-# OPTIONS -W noNoGuardednessFlag #-} in Lib, no options in Ex1, no options in Ex2:
   • Ex1 passes without warnings (✅), and no extra pragma (✅)
   • Ex2 fails termination checking (✅)
   • The error message does not mention --guardedness, instead it just says Problematic calls: loop (🙁)

I'm currently using option (3), but it's easy for clients to forget the {-# OPTIONS --guardedness #-} and get option (4) with a weak error message instead.

I suggest changing when the --guardedness warning is displayed.

Currently, pseudo-code for showing the flag seems to be:

when (checking a record declaration):
    if (record is coinductive && no --guardedness flag):
        warn(... "but option --guardedness is not enabled." ...)

I suggest changing this to:

when (termination checking fails):
    error("Termination checking failed for the following functions:" ...)
    if (call cycle contains a coinductive type X && no --guardedness flag):
        warn(... "but option --guardedness is not enabled." ...)

RetroSearch is an open source project built by @garambo | Open a GitHub Issue

Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo

HTML: 3.2 | Encoding: UTF-8 | Version: 0.7.4