Case splitting fails with fancy types

[david-christiansen]

This is in version 5.0.1 of both the Emacs and Haskell bits. If I load the following file:

{-# LANGUAGE DataKinds, TypeFamilies, TypeOperators, GADTs, KindSignatures #-}

module Vect where

data Nat = Z | S Nat

type family   (n :: Nat) :+ (m :: Nat) :: Nat
type instance Z :+ m = m
type instance S n :+ m = S (n :+ m)

data Vect :: Nat -> * -> * where
  VNil :: Vect Z a
  (:::) :: a -> Vect n a -> Vect (S n) a

vAppend :: Vect n a -> Vect m a -> Vect (n :+ m) a
vAppend x y = _vAppend_body

lAppend :: [a] -> [a] -> [a]
lAppend x y = _lAppend_body

data MyList a = Nil | Cons a (MyList a)

mlAppend :: MyList a -> MyList a -> MyList a
mlAppend x y = _mlAppend_body

and then attempt to case split, I get the following message in the debug buffer:

% split /home/drc/tmp/Vect.hs 24 10
NG BUG: ghc-modi: panic! (the 'impossible' happened)\n  (GHC version 7.8.3 for x86_64-unknown-linux):\n mkHsTyWithBndrs:kvs\n\nPlease report this as a GHC bug:  http://www.haskell.org/ghc/reportabug\n

The List equivalent works fine. I'm mostly used to idris-mode, so I may be doing something wrong here.

[acowley]

I'm not sure where to look for a debug buffer, but ghc-modi crashes when attempting to case-split for me, too. May or may not be the same issue.

[david-christiansen]

You can get a debug buffer by running M-: (setq ghc-debug t) and then
running the command again.

[DanielG]

You can also just run ghc-mod debug in the project directory.

[david-christiansen]

You can also just run ghc-mod debug in the project directory.

Does that work when the error first shows up upon executing a command?

[DanielG]

Yeah debug just displays GHC/cabal version info and such.

[serras]

@acowley Does you bug also happen when pattern matching on a GADT? Maybe the functions I'm calling from the ghc library only work on regular data types. If I had that information, I could check whether I need to change calls for other kinds of data types.

[DanielG]

@serras looks like some HsWithBndrs isnt properly initialized dunno where that's supposed to happen though, also I'm not familiar with the case splitting code.

[alanz]

I have just hit this in https://phabricator.haskell.org/D157, it is a Bool but initialised to an error value in the parser, which means that all OverLit values are dangerous until after the renamer.

You need to be careful not to evaluate ol_type or ol_rebindable.

[acowley]

Thank you @david-christiansen! It's a different error in the first file I tried:

NG BUG: ghc-modi: panic! (the 'impossible' happened)\n  (GHC version 7.8.3 for x86_64-apple-darwin):\n  ForeignImport coercion evaluated before typechecking\n\nPlease report this as a GHC bug:  http://www.haskell.org/ghc/reportabug\n

And another file in the same project doesn't exhibit that error in the same way. So it's more FFI trickiness in my case.

[alanz]

Glad I saw this, need to sort it out in the dev GHC

On Thu, Aug 21, 2014 at 9:14 PM, Anthony Cowley notifications@github.com
wrote:

Thank you @david-christiansen https://github.com/david-christiansen!
It's a different error in the first file I tried:

NG BUG: ghc-modi: panic! (the 'impossible' happened)\n (GHC version 7.8.3
for x86_64-apple-darwin):\n ForeignImport coercion evaluated before
typechecking\n\nPlease report this as a GHC bug:
http://www.haskell.org/ghc/reportabug\n

—
Reply to this email directly or view it on GitHub
#336 (comment)
.

[serras]

The code that is concerned with the error is:

getSrcSpanTypeForFnSplit :: GhcMonad m => G.ModSummary -> Int -> Int -> m (Maybe SplitInfo)
getSrcSpanTypeForFnSplit modSum lineNo colNo = do
    p@ParsedModule{pm_parsed_source = pms} <- G.parseModule modSum
    tcm@TypecheckedModule{tm_typechecked_source = tcs} <- G.typecheckModule p
    let varPat  = find isPatternVar $ listifySpans tcs (lineNo, colNo) :: Maybe (LPat Id)
        match:_ = listifyParsedSpans pms (lineNo, colNo) :: [Gap.GLMatch]
    case varPat of
      Nothing  -> return Nothing
      Just varPat' -> do
        varT <- Gap.getType tcm varPat'  -- Finally we get the type of the var
        case varT of
          Just varT' ->
            let (L matchL (G.Match _ _ (G.GRHSs rhsLs _))) = match
            in return $ Just (SplitInfo (getPatternVarName varPat') matchL varT' (map G.getLoc rhsLs) )
          _ -> return Nothing

In particular, it seems that the error happends in the call to getType, whose text reads:

instance HasType (LPat Id) where
    getType _ (G.L spn pat) = return $ Just (spn, hsPatType pat)

As you can see, I have called the type checker, so it seems to me that everything should be initialized correctly if I've reached that point, including the renamer.

I have found a related bug from doctest sol/doctest#41, where the solution was to add some extra searching for HsWithBndrs. However, I don't understand GHC well enough to know what does it mean.

@alanz @DanielG Any ideas?

[alanz]

I am having a look now

[alanz]

I think the problem arises from

match:_ = listifyParsedSpans pms (lineNo, colNo) :: [Gap.GLMatch]

in getSrcSpanTypeForFnSplit which is calling the ghc-syb-utils version of everythingStaged, which in turn does not dodge all landmines properly.

I put a pull request in recently but @nominolo has not reacted to it yet, see DanielG/ghc-syb#7

I will see if listifySpans can be used instead to get the match

[serras]

@alanz Thanks for taking care and fixig it. Do you know any reference that I could look at to understand what was going on more clearly? All this ghc-syb (or anything in the ghc package) still seems magic to me.

[alanz]

The primary references to SYB are here http://research.microsoft.com/en-us/um/people/simonpj/papers/hmap/

The key thing to it all is how a generic query happens, (which is from
http://hackage.haskell.org/package/syb-0.4.2/docs/src/Data-Generics-Aliases.html#mkQ)

-- | Make a generic query;
--   start from a type-specific case;
--   return a constant otherwise
--
mkQ :: ( Typeable a
       , Typeable b
       )
    => r
    -> (b -> r)
    -> a
    -> r
(r `mkQ` br) a = case cast a of
                        Just b  -> br b
                        Nothing -> r

which makes use of the type safe cast from Data.Data
http://hackage.haskell.org/package/base-4.7.0.1/docs/src/Data-Typeable.html#cast

-- | The type-safe cast operation
cast :: forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast x = if typeRep (Proxy :: Proxy a) == typeRep (Proxy :: Proxy b)
           then Just $ unsafeCoerce x
           else Nothing

In other words it makes use of the metadata provided by the fact that a given x is an instance of Typeable to check if they are the same type, and if so does an unsafeCoerce, which is not in fact unsafe because of the check that the types are the same.

In a similar fashion traversals are defined which can apply the generic query to all the immediate subterms of a given data item.

The problem comes with the GHC AST which does things like

data HsWithBndrs thing
  = HsWB { hswb_cts :: thing         -- Main payload (type or list of types)
         , hswb_kvs :: [Name]        -- Kind vars
         , hswb_tvs :: [Name]        -- Type vars
    }                  
  deriving (Data, Typeable)

mkHsWithBndrs :: thing -> HsWithBndrs thing
mkHsWithBndrs x = HsWB { hswb_cts = x, hswb_kvs = panic "mkHsTyWithBndrs:kvs"
                                     , hswb_tvs = panic "mkHsTyWithBndrs:tvs" }

So that instead of having the expected [Name] value which the syb traversal can deal with, we end up evaluating a panic call which is just a GHC specific kind of error.

So the ghc-syb package provides traversals that have knowledge of where these landmines are, and can tiptoe around them without evaluating the embedded panics.

Unfortunately the original did not cover all of the panic situations, and GHC 7.8.3 brought in some more.

Hence your problem.