Compile regression with Singletons-2.0

[crockeea]

The following code compiled with singletons-1.0

{-# LANGUAGE DataKinds,
             GADTs, KindSignatures, PolyKinds,
             ScopedTypeVariables, TemplateHaskell, TypeFamilies,
             UndecidableInstances #-}

module SingTest where

import Data.Singletons.Prelude
import Data.Singletons.TH
import Data.Type.Natural

(<<=) :: Nat -> Nat -> Bool
Z   <<= _   = True
S _ <<= Z   = False
S n <<= S m = n <<= m

singletons [d|
            newtype PrimePower = PP (Nat,Nat)
            |]

-- SMART CONSTRUCTORS
singletons [d|

            ppMul :: PrimePower -> [PrimePower] -> [PrimePower]
            ppMul x [] = [x]
            ppMul (PP(p,e)) (PP (p',e'):pps')
                | p == p' = PP(p,e + e'):pps'
                | p <<= p' = (PP(p,e)):(PP (p',e'):pps')
                | otherwise = (PP(p',e')):ppMul (PP(p,e)) pps'
            |]

but fails with singletons-2.0. It seems that the interaction between multiple patterns and guards causes the error:

    Could not deduce (PpMul arg_16274411810 arg_16274411830
                      ~ Case_1627441197
                          arg_16274411810
                          arg_16274411830
                          (Tuple2Sym2 arg_16274411810 arg_16274411830))
    from the context (t0 ~ arg_16274411810, t1 ~ arg_16274411830)
      bound by the type signature for
                 lambda_adl5 :: (t0 ~ arg_16274411810, t1 ~ arg_16274411830) =>
                                Sing arg_16274411810
                                -> Sing arg_16274411830
                                -> Sing (Apply (Apply PpMulSym0 arg_16274411810) arg_16274411830)
      at Main.hs:(22,1)-(38,14)
    Expected type: Sing
                     (Apply (Apply PpMulSym0 arg_16274411810) arg_16274411830)
      Actual type: Sing
                     (Case_1627441197
                        arg_16274411810
                        arg_16274411830
                        (Apply (Apply Tuple2Sym0 arg_16274411810) arg_16274411830))

The following works in both singletons versions:

ppMul :: PrimePower -> [PrimePower] -> [PrimePower]
            ppMul x [] = [x]
            ppMul (PP(p,e)) (PP (p',e'):pps') =
              if p == p' then PP(p,e + e'):pps'
              else if p <<= p' then (PP(p,e)):(PP (p',e'):pps')
              else (PP(p',e')):ppMul (PP(p,e)) pps'

[goldfirere]

Without looking at this in depth, I think the fact that the code worked in singletons-1.0 is a lucky fluke. Overlapped patterns (like | otherwise) generally fail to singletonize. (Promotion should work fine, though.)

This would be fixed by match flattening (that is, convert overlapping patterns into non-overlapping patterns). This is actually implemented, but is incredibly slow. So slow that many machines would fail to compile Data.Singletons.Prelude.List. So it's disabled. But I have not had time to investigate the slowdown in depth enough to figure out what to do about it. Care to lend a hand? The ticket tracking this all is #113, where I'll post shortly.

[crockeea]

Actually, you can remove the "otherwise" case (or even the bottom two guards), and the code still works in 1.0 but not 2.0. Is there still overlap somewhere else?

[goldfirere]

Hm. Do you have a self-standing test case? I don't have Data.Type.Natural.

[crockeea]

{-# LANGUAGE DataKinds,
             GADTs, KindSignatures, PolyKinds,
             ScopedTypeVariables, TemplateHaskell, TypeFamilies,
             UndecidableInstances #-}

import Data.Singletons.Prelude
import Data.Singletons.TH

singletons [d|
            newtype PrimePower = PP (Bool, Bool)
            |]

-- SMART CONSTRUCTORS
singletons [d|

            ppMul :: PrimePower -> [PrimePower] -> [PrimePower]
            ppMul x [] = [x]
            ppMul (PP(p,e)) (PP (p',e'):pps')
                | p == p' = PP(p,e):pps'
            |]

[goldfirere]

Unfortunately, this still presents as an overlapping pattern. Consider desugaring guards. We want to write a new sequence of function clauses, without guards, that means the same as an original sequence of function clauses, perhaps with guards. We end up with nested case statements. The problem is that future function clauses might match arguments that don't match the clause under consideration. So the first step of this transformation is to make a guarded function clause universal, and then deal with any remaining function clauses later. And, here, we get an overlapping pattern again.

I don't see any good way of avoiding this without match flattening, I'm afraid.

[crockeea]

Okay, if this falls into a known category, that's a good start!