Using the solver seems to break GHC

leonschoorl commented 5 years ago

@kozross reported this in clash-lang/ghc-typelits-knownnat#28:

Consider the following:
{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}
{-# OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE GADTs #-}

module Data.Ordinal where

import GHC.TypeNats

data Ordinal (n :: Nat) where
  Ordinal :: (KnownNat n, 1 <= n) => Integer -> Ordinal n

exponentiate :: forall (n :: Nat) (m :: Nat) . Ordinal n -> Ordinal m -> Ordinal ((n - 1) ^ (m - 1) + 1)
exponentiate (Ordinal x) (Ordinal y) = Ordinal _
If you attempt to compile this with GHC 8.6.5 (as well as 8.8.1 and 8.4.4), you will get this error:
ghc: panic! (the 'impossible' happened)
  (GHC version 8.6.5 for x86_64-unknown-linux):
  Prelude.foldr1: empty list

Please report this as a GHC bug:  http://www.haskell.org/ghc/reportabug
However, if I disable both solvers (by commenting out the first two lines), I don't get this.

I'm unsure if this is an issue with one solver, both solvers, GHC itself, or some combination, but I figured I'd report it just in case.

Edit: Found a smaller case, eliminating any concern regarding integer-gmp.

leonschoorl commented 5 years ago

https://github.com/clash-lang/ghc-typelits-natnormalise/blob/de878d1309531960dd7c6e70cb3ab6ace63f19e9/src/GHC/TypeLits/Normalise/SOP.hs#L278-L279 This ends up being called with i = -1

kozross commented 5 years ago

@leonschoorl Thanks for reporting this in the right place - I wasn't sure which one of the two was having the issue.

clash-lang / ghc-typelits-natnormalise

Using the solver seems to break GHC #28