Changes between Initial Version and Version 1 of Ticket #9918, comment 16


Ignore:
Timestamp:
Jan 5, 2015 4:08:38 PM (5 years ago)
Author:
simonpj
Comment:

Legend:

Unmodified
Added
Removed
Modified
  • Ticket #9918, comment 16

    initial v1  
    22> The straw-man proposal is that with `{-# UNDECIDABLE #-}` (or some other pragma name) on a closed type family, the surely-apart check is strengthened, allowing more reductions to fire.
    33
    4 This seems to be precisely my {-# UNSAFE_STRONGER_APARTNESS_CHECK #-}` pragma. Declaring this property of a type function seems orthogonal to whether or not evaluating the function terminates -- I could see both `{-# UNDECIDABLE #-}` and `{-# UNSAFE_STRONGER_APARTNESS_CHECK #-}` as separate pragmas, where neither implies the other. The first means that GHC might not terminate; the second means your program might not be type-safe.
     4This seems to be precisely my `{-# UNSAFE_STRONGER_APARTNESS_CHECK #-}` pragma. Declaring this property of a type function seems orthogonal to whether or not evaluating the function terminates -- I could see both `{-# UNDECIDABLE #-}` and `{-# UNSAFE_STRONGER_APARTNESS_CHECK #-}` as separate pragmas, where neither implies the other. The first means that GHC might not terminate; the second means your program might not be type-safe.
    55
    66>