
#10180: Lint check: Empty alternatives imply bottoming scrutinee -------------------------------------+------------------------------------- Reporter: nomeata | Owner: nomeata Type: task | Status: infoneeded Priority: normal | Milestone: Component: Compiler | Version: 7.11 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: None/Unknown | Unknown/Multiple Blocked By: | Test Case: Related Tickets: | Blocking: | Differential Revisions: -------------------------------------+------------------------------------- Comment (by nomeata): There is no end of reasons why something diverges: {{{ =====> T2431(normal) 339 of 4438 [0, 0, 0] cd ./deSugar/should_compile && "/home/jojo/build/haskell/ghc- validate/inplace/bin/ghc-stage2" -c T2431.hs -fforce-recomp -dcore-lint -dcmm-lint -dno-debug-output -no-user-package-db -rtsopts -fno-warn-tabs -fno-ghci-history -ddump-simpl -dsuppress-uniques > T2431.comp.stderr 2>&1 Compile failed (status 256) errors were: *** Core Lint errors : in result of Simplifier *** T2431.hs:8:8: Warning: [in body of lambda with binder x :: Int :~: Bool] No alternatives for a case scrutinee not known to diverge for sure: x *** Offending Program *** absurd :: forall a. Int :~: Bool -> a [LclIdX, Arity=1, Str=DmdType, Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True, WorkFree=True, Expandable=True, Guidance=ALWAYS_IF(arity=1,unsat_ok=True,boring_ok=True)}] absurd = \ (@ a) (x :: Int :~: Bool) -> case x of _ [Occ=Dead] { } *** End of Offense *** }}} I’m beginning to wonder if the lint rule is a good idea. After all, by trying to add such a rule we are saying “definite divergence must be obvious”, and hence we would be precluding the compiler to derive and use definite divergence that is non-obvious, or that was obvious at one point in the pipeline, but isn’t any more later when the linter runs. Here is an example of non-trivially always empty types: `Void` wrapped deeply in some strict data type. Or even `Void` as the result of a type function wrapped deeply in some strict data type. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10180#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler