Skip to content

-fdefer-type-errors doesn't produce a warning

With the attached code I get the expected error

sing.hs:20:8:
    Couldn't match type 'False with 'True
    Inaccessible code in
      the type signature for
        nth :: (k :< n) ~ 'True => Vec a n -> SNat k -> a

However, if I compile with -fdefer-type-errors, compilation goes clean without any errors or warnings.

Also, if I comment out the last line (with inaccessible code) and compile with -fforce-recomp -fwarn-incomplete-patterns, then I get a false warning

sing.hs:21:1: Warning:
    Pattern match(es) are non-exhaustive
    In an equation for `nth': Patterns not matched: Nil _
Trac metadata
Trac field Value
Version 7.6.1
Type Bug
TypeOfFailure OtherFailure
Priority normal
Resolution Unresolved
Component Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC roma@ro-che.info
Operating system
Architecture
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information