switch must be exhaustive, consider adding a default clause

Drew_Crawford · April 8, 2017, 6:29pm

Is there a good reason we do not compile this:

import UIKit

func foo(operation: UINavigationControllerOperation) {
switch(operation) {
case .push: /* snip */ break
case .pop: /* snip */ break
default:
preconditionFailure("This is a silly operation")
}
switch(operation) {
case .push: /* snip */ break
case .pop: /* snip */ break
//error: Switch must be exhaustive, consider adding a default clause
}
}
The switch *is* exhaustive, because the default case is unreachable. The compiler could infer as much from branch analysis.

Josh_Parmenter · April 10, 2017, 4:18pm

case .none isn’t handled.
This should probably be on the swift-users list though, no?
Best,
Josh

···

On Apr 8, 2017, at 11:29 AM, Drew Crawford via swift-evolution <swift-evolution@swift.org<mailto:swift-evolution@swift.org>> wrote:

Is there a good reason we do not compile this:

import UIKit

func foo(operation: UINavigationControllerOperation) {
    switch(operation) {
    case .push: /* snip */ break
    case .pop: /* snip */ break
    default:
        preconditionFailure("This is a silly operation")
    }
    switch(operation) {
        case .push: /* snip */ break
        case .pop: /* snip */ break
         //error: Switch must be exhaustive, consider adding a default clause
    }
}

The switch *is* exhaustive, because the default case is unreachable. The compiler could infer as much from branch analysis.

_______________________________________________
swift-evolution mailing list
swift-evolution@swift.org<mailto:swift-evolution@swift.org>
https://lists.swift.org/mailman/listinfo/swift-evolution

Joshua Parmenter | Engineering Lead, Apple Technologies

T 248 777 7777
C 206 437 1551
F 248 616 1980
www.vectorform.com<http://www.vectorform.com/>

Vectorform
2107 Elliott Ave Suite 303
Seattle, WA 98121 USA

Think Tank. Lab. Studio.
We invent digital products and experiences.

SEATTLE | DETROIT | NEW YORK | MUNICH | HYDERABAD

Joe_Groff · April 11, 2017, 4:38pm

By design, Swift avoids making semantic rules based on that kind of analysis, since it would be brittle and difficult to describe when the compiler can and can't see that a condition holds nonlocally like this.

-Joe

···

On Apr 8, 2017, at 11:29 AM, Drew Crawford via swift-evolution <swift-evolution@swift.org> wrote:

Is there a good reason we do not compile this:

import UIKit

func foo(operation: UINavigationControllerOperation) {
    switch(operation) {
    case .push: /* snip */ break
    case .pop: /* snip */ break
    default:
        preconditionFailure("This is a silly operation")
    }
    switch(operation) {
        case .push: /* snip */ break
        case .pop: /* snip */ break
         //error: Switch must be exhaustive, consider adding a default clause
    }
}
The switch *is* exhaustive, because the default case is unreachable. The compiler could infer as much from branch analysis

knatt · April 10, 2017, 4:53pm

case .none isn’t handled.

It shouldn’t need to be handled in the second switch because it’s impossible. Not just developer thinks “impossible” but easily provable by static analysis the compiler is doing it anyway—I wouldn’t be surprised if including the case resulted in an “unreachable code” warning (in fact, it probably should).

This should probably be on the swift-users list though, no?

File a bug, IMO.

···

On Apr 10, 2017, at 9:18 AM, Josh Parmenter via swift-evolution <swift-evolution@swift.org> wrote:

Best,
Josh

On Apr 8, 2017, at 11:29 AM, Drew Crawford via swift-evolution <swift-evolution@swift.org <mailto:swift-evolution@swift.org><mailto:swift-evolution@swift.org <mailto:swift-evolution@swift.org>>> wrote:

Is there a good reason we do not compile this:

import UIKit

func foo(operation: UINavigationControllerOperation) {
   switch(operation) {
   case .push: /* snip */ break
   case .pop: /* snip */ break
   default:
       preconditionFailure("This is a silly operation")
   }
   switch(operation) {
       case .push: /* snip */ break
       case .pop: /* snip */ break
        //error: Switch must be exhaustive, consider adding a default clause
   }
}

The switch *is* exhaustive, because the default case is unreachable. The compiler could infer as much from branch analysis.

_______________________________________________
swift-evolution mailing list
swift-evolution@swift.org <mailto:swift-evolution@swift.org><mailto:swift-evolution@swift.org <mailto:swift-evolution@swift.org>>
https://lists.swift.org/mailman/listinfo/swift-evolution

Joshua Parmenter | Engineering Lead, Apple Technologies

T 248 777 7777
C 206 437 1551
F 248 616 1980
www.vectorform.com <http://www.vectorform.com/><http://www.vectorform.com/>

Vectorform
2107 Elliott Ave Suite 303
Seattle, WA 98121 USA

Think Tank. Lab. Studio.
We invent digital products and experiences.

SEATTLE | DETROIT | NEW YORK | MUNICH | HYDERABAD
_______________________________________________
swift-evolution mailing list
swift-evolution@swift.org <mailto:swift-evolution@swift.org>
https://lists.swift.org/mailman/listinfo/swift-evolution

Josh_Parmenter · April 10, 2017, 4:58pm

case .none isn’t handled.

It shouldn’t need to be handled in the second switch because it’s impossible. Not just developer thinks “impossible” but easily provable by static analysis the compiler is doing it anyway—I wouldn’t be surprised if including the case resulted in an “unreachable code” warning (in fact, it probably should).

Why? Because of preconditionFailure? That COULD be optimized out as per this documentation:

/// * In `-Ounchecked` builds, the optimizer may assume that this function is
/// never called. Failure to satisfy that assumption is a serious
/// programming error.

So I’m not sure if that is the case or not.

This should probably be on the swift-users list though, no?

File a bug, IMO.

Yes - it should probably be looked at by someone who would know if this a bug or the expected behavior.

Best,
Josh

···

On Apr 10, 2017, at 9:53 AM, Kevin Nattinger <swift@nattinger.net<mailto:swift@nattinger.net>> wrote:
On Apr 10, 2017, at 9:18 AM, Josh Parmenter via swift-evolution <swift-evolution@swift.org<mailto:swift-evolution@swift.org>> wrote:

On Apr 8, 2017, at 11:29 AM, Drew Crawford via swift-evolution <swift-evolution@swift.org<mailto:swift-evolution@swift.org><mailto:swift-evolution@swift.org>> wrote:

Is there a good reason we do not compile this:

import UIKit

func foo(operation: UINavigationControllerOperation) {
   switch(operation) {
   case .push: /* snip */ break
   case .pop: /* snip */ break
   default:
       preconditionFailure("This is a silly operation")
   }
   switch(operation) {
       case .push: /* snip */ break
       case .pop: /* snip */ break
        //error: Switch must be exhaustive, consider adding a default clause
   }
}

The switch *is* exhaustive, because the default case is unreachable. The compiler could infer as much from branch analysis.

_______________________________________________
swift-evolution mailing list
swift-evolution@swift.org<mailto:swift-evolution@swift.org><mailto:swift-evolution@swift.org>
https://lists.swift.org/mailman/listinfo/swift-evolution

Joshua Parmenter | Engineering Lead, Apple Technologies

T 248 777 7777
C 206 437 1551
F 248 616 1980
www.vectorform.com<http://www.vectorform.com/><http://www.vectorform.com/>

Vectorform
2107 Elliott Ave Suite 303
Seattle, WA 98121 USA

Think Tank. Lab. Studio.
We invent digital products and experiences.

SEATTLE | DETROIT | NEW YORK | MUNICH | HYDERABAD
_______________________________________________
swift-evolution mailing list
swift-evolution@swift.org<mailto:swift-evolution@swift.org>
https://lists.swift.org/mailman/listinfo/swift-evolution

Drew_Crawford · April 11, 2017, 6:24pm

By design, Swift avoids making semantic rules based on that kind of analysis, since it would be brittle and difficult to describe when the compiler can and can't see that a condition holds nonlocally like this.
Swift *currently implements* semantic rules based on this kind of analysis. Exhibit A:

func foo() {

let a: Bool

if UUID\(\)\.uuidString == &quot;non\-local condition&quot; \{

    a = true

\}

else \{

    preconditionFailure\(&quot;Don&#39;t initialize a&quot;\)

\}

print\(&quot;\\\(a\)&quot;\) //NOT: error: a is uninitialized

}

···

On April 11, 2017 at 11:38:05 AM, Joe Groff (jgroff@apple.com) wrote:

codafi · April 11, 2017, 11:00pm

What Joe is referring to is the kind of refinement-style rules that would be necessary to teach the type checker about how to that kind of analysis. Right now, all our switch analysis, and even this example, are just DI and control-flow checks.

···

On Apr 11, 2017, at 2:24 PM, Drew Crawford via swift-evolution <swift-evolution@swift.org> wrote:

On April 11, 2017 at 11:38:05 AM, Joe Groff (jgroff@apple.com <mailto:jgroff@apple.com>) wrote:

By design, Swift avoids making semantic rules based on that kind of analysis, since it would be brittle and difficult to describe when the compiler can and can't see that a condition holds nonlocally like this.

Swift *currently implements* semantic rules based on this kind of analysis. Exhibit A:

func foo() {

    let a: Bool

    if UUID().uuidString == "non-local condition" {

        a = true

    }

    else {

        preconditionFailure("Don't initialize a")

    }

    print("\(a)") //NOT: error: a is uninitialized

}

_______________________________________________
swift-evolution mailing list
swift-evolution@swift.org <mailto:swift-evolution@swift.org>
https://lists.swift.org/mailman/listinfo/swift-evolution

Joe_Groff · April 12, 2017, 8:17pm

That analysis is pretty strictly limited as well. The DI assignment has to happen once along every code path before the variable is ever read or escaped, so the effects are localized. To do pattern matching refinement something like you're proposing, we need to know that the value isn't mutated between switches. That becomes impossible if the variable is ever escaped, so you'd get spooky action at a distance where referencing the variable in a closure somewhere would cause seemingly-unrelated control flow errors to spring up seeming randomly; global variables and class properties would also fundamentally never benefit from this analysis, making it feel inconsistent when exactly the refined switch is allowed.

-Joe

···

On Apr 11, 2017, at 11:24 AM, Drew Crawford <drew@drewcrawfordapps.com> wrote:

On April 11, 2017 at 11:38:05 AM, Joe Groff (jgroff@apple.com <mailto:jgroff@apple.com>) wrote:

By design, Swift avoids making semantic rules based on that kind of analysis, since it would be brittle and difficult to describe when the compiler can and can't see that a condition holds nonlocally like this.

Swift *currently implements* semantic rules based on this kind of analysis. Exhibit A:

func foo() {

    let a: Bool

    if UUID().uuidString == "non-local condition" {

        a = true

    }

    else {

        preconditionFailure("Don't initialize a")

    }

    print("\(a)") //NOT: error: a is uninitialized

}