search

clash-lang / ghc-typelits-knownnat

Derive KnownNat constraints from other KnownNat constraints
Other
14 stars 10 forks source link

Using the solver seems to break GHC #28

Closed kozross closed 5 years ago

kozross commented 5 years ago

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

Thanks for the report!

While this happens both through ghc-typelits-natnormalise and ghc-typelits-knownat the actual problem is somewhere in natnormalise. So I'll reopen this issue over there.