[GHC] #13943: Compiler infinite loop with GHC-8.2

[GHC]

#13943: Compiler infinite loop with GHC-8.2
-------------------------------------+-------------------------------------
        Reporter:  vagarenko         |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  high              |            Milestone:  8.2.1
       Component:  Compiler          |              Version:  8.2.1-rc3
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:  #12791            |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by mpickering):

 The problem is that we are repeatedly able to solves constraints of the
 form `Take (k - 1)` with the dictionary we have for `Take n` which matches
 any constraint. We loop forever as we track whether we have previously
 solved precisely the same constraint rather than used the same dictionary
 before. I am not sure exactly how best to fix this.

 This code does use `UndecidableInstances` so it is perhaps not entirely
 our responsibility to ensure termination but it has not yet been ruled how
 this flag should interact with `UndecidableInstances`.


 As an aside, you can also write your program like this which avoids
 overlapping and undecidable instances by making the recursion clear from
 the types but admittedly, it is not very convenient to write numbers like
 this.

 {{{
 {-# LANGUAGE MultiParamTypeClasses   #-}
 {-# LANGUAGE TypeOperators           #-}
 {-# LANGUAGE FlexibleInstances       #-}
 {-# LANGUAGE FlexibleContexts        #-}
 {-# LANGUAGE ScopedTypeVariables     #-}
 {-# LANGUAGE TypeApplications        #-}
 {-# LANGUAGE TypeInType              #-}
 {-# LANGUAGE AllowAmbiguousTypes     #-}
 {-# LANGUAGE NoImplicitPrelude       #-}
 {-# LANGUAGE GADTs                   #-}

 module Data.List.Unrolled where

 import GHC.TypeLits

 data N = Z | S N

 -- | Drop @n@ elements from a list
 class Drop (n :: N) where
     drop :: [a] -> [a]

 instance Drop Z where
     drop xs = xs
     {-# INLINE drop #-}

 instance (Drop n) => Drop (S n) where
     drop [] = []
     drop (_ : xs) = drop @n xs
     {-# INLINE drop #-}

 -- | Take @n@ elements from a list
 class Take (n :: N) where
     take :: [a] -> [a]

 instance Take Z where
     take _ = []
     {-# INLINE take #-}

 instance (Take n) => Take (S n) where
     take [] = []
     take (x : xs) = x : take @n xs
     {-# INLINE take #-}

 -- | Split list at @n at -th element.
 splitAt :: forall (n :: N) a. (Take n, Drop n) => [a] -> ([a], [a])
 splitAt xs = (take @n xs, drop @n xs)

 -- | Split list into chunks of the given length @c at . @n@ is length of the
 list.
 class ChunksOf (n :: N) (c :: N) where
     chunksOf :: [a] -> [[a]]

 instance ChunksOf Z c where
     chunksOf _ = []
     {-# INLINE chunksOf #-}

 instance (Take c, Drop c, ChunksOf n c) => ChunksOf (S n) c where
     chunksOf xs =
         let (l, r) = splitAt @c xs
         in l : chunksOf @n @c r
     {-# INLINE chunksOf #-}

 }}}

-- 
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/13943#comment:3>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler